From 8888a5bd5c4b5438a0a6b5778a21af52bd69dedf Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Wed, 16 Oct 2024 13:40:53 +0200 Subject: [PATCH] Reduce ax-10, ax-11, ax-12 usage (#4292) * Reduce axiom usage * avoid ax-12 in csbconstg * avoid ax-10, ax-11, ax-12 in csbie * avoid ax-10, ax-11, ax-12 in csbied * add unabw, add notabw * use unabw in dfif6 to avoid ax-10, ax-12 * use notabw in dfif3 to avoid ax-10, ax-12 * avoid ax-10,ax-11,ax-12 in cbvopabv * use unabw in unopab to avoid ax-10, ax-12 * add tags * rewrap * restore opeq1 and opeq2 proofs * restore csb0 proof * add $j tags --- discouraged | 14 ++-- set.mm | 186 ++++++++++++++++++++++++++++++++++------------------ 2 files changed, 129 insertions(+), 71 deletions(-) diff --git a/discouraged b/discouraged index 7202f6f6ba..aa87a16201 100644 --- a/discouraged +++ b/discouraged @@ -14855,6 +14855,7 @@ New usage of "cbvmptfg" is discouraged (1 uses). New usage of "cbvmptg" is discouraged (1 uses). New usage of "cbvmptvg" is discouraged (0 uses). New usage of "cbvopab1g" is discouraged (1 uses). +New usage of "cbvopabvOLD" is discouraged (0 uses). New usage of "cbvrab" is discouraged (0 uses). New usage of "cbvrabcsf" is discouraged (1 uses). New usage of "cbvrabv2" is discouraged (0 uses). @@ -15289,12 +15290,14 @@ New usage of "crhmsubcALTV" is discouraged (1 uses). New usage of "cringcALTV" is discouraged (9 uses). New usage of "cringcatALTV" is discouraged (0 uses). New usage of "crngcALTV" is discouraged (7 uses). -New usage of "csb0OLD" is discouraged (0 uses). New usage of "csbcnvgALT" is discouraged (0 uses). New usage of "csbco" is discouraged (1 uses). New usage of "csbco3g" is discouraged (0 uses). +New usage of "csbconstgOLD" is discouraged (0 uses). New usage of "csbeq2gVD" is discouraged (0 uses). New usage of "csbfv12gALTVD" is discouraged (0 uses). +New usage of "csbieOLD" is discouraged (0 uses). +New usage of "csbiedOLD" is discouraged (0 uses). New usage of "csbima12gALTVD" is discouraged (0 uses). New usage of "csbingVD" is discouraged (0 uses). New usage of "csbnestg" is discouraged (1 uses). @@ -17712,8 +17715,6 @@ New usage of "opabresidOLD" is discouraged (1 uses). New usage of "opelcn" is discouraged (1 uses). New usage of "opelopab4" is discouraged (0 uses). New usage of "opelreal" is discouraged (8 uses). -New usage of "opeq1OLD" is discouraged (0 uses). -New usage of "opeq2OLD" is discouraged (0 uses). New usage of "opidon2OLD" is discouraged (1 uses). New usage of "opidonOLD" is discouraged (2 uses). New usage of "opnmblALT" is discouraged (0 uses). @@ -19261,6 +19262,7 @@ Proof modification of "cbveuwOLD" is discouraged (29 steps). Proof modification of "cbvexsv" is discouraged (29 steps). Proof modification of "cbviotavwOLD" is discouraged (12 steps). Proof modification of "cbvmowOLD" is discouraged (62 steps). +Proof modification of "cbvopabvOLD" is discouraged (20 steps). Proof modification of "cbvralfwOLD" is discouraged (139 steps). Proof modification of "cbvreuvwOLD" is discouraged (13 steps). Proof modification of "cbvriotavwOLD" is discouraged (13 steps). @@ -19313,10 +19315,12 @@ Proof modification of "conventions" is discouraged (1 steps). Proof modification of "conventions-comments" is discouraged (1 steps). Proof modification of "conventions-labels" is discouraged (1 steps). Proof modification of "copsex2gOLD" is discouraged (119 steps). -Proof modification of "csb0OLD" is discouraged (19 steps). Proof modification of "csbcnvgALT" is discouraged (112 steps). +Proof modification of "csbconstgOLD" is discouraged (8 steps). Proof modification of "csbeq2gVD" is discouraged (61 steps). Proof modification of "csbfv12gALTVD" is discouraged (322 steps). +Proof modification of "csbieOLD" is discouraged (10 steps). +Proof modification of "csbiedOLD" is discouraged (16 steps). Proof modification of "csbima12gALTVD" is discouraged (148 steps). Proof modification of "csbingVD" is discouraged (256 steps). Proof modification of "csbopabgALT" is discouraged (85 steps). @@ -20127,8 +20131,6 @@ Proof modification of "onfrALTlem5VD" is discouraged (320 steps). Proof modification of "onnevOLD" is discouraged (26 steps). Proof modification of "opabresidOLD" is discouraged (50 steps). Proof modification of "opelopab4" is discouraged (69 steps). -Proof modification of "opeq1OLD" is discouraged (73 steps). -Proof modification of "opeq2OLD" is discouraged (68 steps). Proof modification of "opidon2OLD" is discouraged (80 steps). Proof modification of "opidonOLD" is discouraged (198 steps). Proof modification of "opnmblALT" is discouraged (332 steps). diff --git a/set.mm b/set.mm index 26c68a75a6..788190d211 100644 --- a/set.mm +++ b/set.mm @@ -36402,11 +36402,24 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use $} ${ - $d B x $. + $d B x y z $. $d A y $. $( Substitution doesn't affect a constant ` B ` (in which ` x ` does not occur). ~ csbconstgf with distinct variable requirement. (Contributed - by Alan Sare, 22-Jul-2012.) $) + by Alan Sare, 22-Jul-2012.) Avoid ~ ax-12 . (Revised by Gino Giotto, + 15-Oct-2024.) $) csbconstg $p |- ( A e. V -> [_ A / x ]_ B = B ) $= + ( vy vz cv csb wceq csbeq1 eqeq1d wcel wsbc cab df-csb cvv sbcg elv abbii + wb abid2 3eqtri vtoclg ) AEGZCHZCIABCHZCIEBDUDBIUEUFCAUDBCJKUEFGCLZAUDMZF + NUGFNCAFUDCOUHUGFUHUGTEUGAUDPQRSFCUAUBUC $. + $( $j usage 'csbconstg' avoids 'ax-10' 'ax-11' 'ax-12'; $) + $} + + ${ + $d B x $. + $( Obsolete version of ~ csbconstg as of 15-Oct-2024. (Contributed by Alan + Sare, 22-Jul-2012.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + csbconstgOLD $p |- ( A e. V -> [_ A / x ]_ B = B ) $= ( nfcv csbconstgf ) ABCDACEF $. $} @@ -36589,23 +36602,54 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use $} ${ - $d x A $. $d x C $. + $d x y A $. $d x y z C $. $d B y z $. csbie.1 $e |- A e. _V $. csbie.2 $e |- ( x = A -> B = C ) $. $( Conversion of implicit substitution to explicit substitution into a - class. (Contributed by AV, 2-Dec-2019.) $) + class. (Contributed by AV, 2-Dec-2019.) Reduce axiom usage. (Revised + by Gino Giotto, 15-Oct-2024.) $) csbie $p |- [_ A / x ]_ B = C $= + ( vy csb cv wcel wsbc cab df-csb wceq eleq2d sbcie abbii abid2 3eqtri ) A + BCHGIZCJZABKZGLTDJZGLDAGBCMUBUCGUAUCABEAIBNCDTFOPQGDRS $. + $( $j usage 'csbie' avoids 'ax-10' 'ax-11' 'ax-12'; $) + $} + + ${ + $d x A $. $d x C $. + csbieOLD.1 $e |- A e. _V $. + csbieOLD.2 $e |- ( x = A -> B = C ) $. + $( Obsolete version of ~ csbie as of 15-Oct-2024. (Contributed by AV, + 2-Dec-2019.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + csbieOLD $p |- [_ A / x ]_ B = C $= ( nfcv csbief ) ABCDEADGFH $. $} ${ - $d x A $. $d x C $. $d x ph $. + $d x y z A $. $d B y z $. $d x y z C $. $d x z ph $. csbied.1 $e |- ( ph -> A e. V ) $. csbied.2 $e |- ( ( ph /\ x = A ) -> B = C ) $. $( Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario - Carneiro, 13-Oct-2016.) $) + Carneiro, 13-Oct-2016.) Reduce axiom usage. (Revised by Gino Giotto, + 15-Oct-2024.) $) csbied $p |- ( ph -> [_ A / x ]_ B = C ) $= + ( vy vz csb cv wcel wsbc cab df-csb wb wal wceq wa eleq2d alrimiv df-clab + sbcied wsb eleq1w sbcbidv sbievw bitr2i bibi1i biimpi sylg dfcleq sylibr + weq syl5eq ) ABCDKILDMZBCNZIOZEBICDPAJLZUSMZUTEMZQZJRUSESAUTDMZBCNZVBQZVC + JAVFJAVDVBBCFGABLCSTDEUTHUAUDUBVFVCVEVAVBVAURIJUEVEURJIUCURVEIJIJUOUQVDBC + IJDUFUGUHUIUJUKULJUSEUMUNUP $. + $( $j usage 'csbied' avoids 'ax-10' 'ax-11' 'ax-12'; $) + $} + + ${ + $d x A $. $d x C $. $d x ph $. + csbiedOLD.1 $e |- ( ph -> A e. V ) $. + csbiedOLD.2 $e |- ( ( ph /\ x = A ) -> B = C ) $. + $( Obsolete version of ~ csbied as of 15-Oct-2024. (Contributed by Mario + Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + csbiedOLD $p |- ( ph -> [_ A / x ]_ B = C ) $= ( nfv nfcvd csbiedf ) ABCDEFABIABEJGHK $. $} @@ -39546,6 +39590,20 @@ technically classes despite morally (and provably) being sets, like ` 1 ` -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) + ${ + $d x y $. $d ph y $. $d ps y $. $d ch x $. $d th x $. + unabw.1 $e |- ( x = y -> ( ph <-> ch ) ) $. + unabw.2 $e |- ( x = y -> ( ps <-> th ) ) $. + $( Union of two class abstractions. Version of ~ unab using implicit + substitution, which does not require ~ ax-8 , ~ ax-10 , ~ ax-12 . + (Contributed by Gino Giotto, 15-Oct-2024.) $) + unabw $p |- ( { x | ph } u. { x | ps } ) = { y | ( ch \/ th ) } $= + ( cab cun cv wcel wo df-un wsb df-clab sbievw bitri orbi12i abbii eqtri ) + AEIZBEIZJFKZUBLZUDUCLZMZFICDMZFIFUBUCNUGUHFUECUFDUEAEFOCAFEPACEFGQRUFBEFO + DBFEPBDEFHQRSTUA $. + $( $j usage 'unabw' avoids 'df-clel' 'ax-8' 'ax-10' 'ax-11' 'ax-12'; $) + $} + ${ $d x y $. $d ph y $. $d ps y $. $( Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) @@ -39582,6 +39640,19 @@ technically classes despite morally (and provably) being sets, like ` 1 ` ( wa simpr ss2abi ) ABDBCABEF $. $} + ${ + $d x y $. $d y ph $. $d x ps $. + notabw.1 $e |- ( x = y -> ( ph <-> ps ) ) $. + $( A class abstraction defined by a negation. Version of ~ notab using + implicit substitution, which does not require ~ ax-10 , ~ ax-12 . + (Contributed by Gino Giotto, 15-Oct-2024.) $) + notabw $p |- { x | -. ph } = ( _V \ { y | ps } ) $= + ( wn cab cv cvv wcel wa cdif vex biantrur wsb df-clab weq bicomd equcoms + wb sbievw bitri xchnxbi abbii df-dif eqtr4i ) AFZCGCHZIJZUHBDGZJZFZKZCGIU + JLUGUMCUKUMAUIULCMNUKBDCOABCDPBADCBATCDCDQABERSUAUBUCUDCIUJUEUF $. + $( $j usage 'notabw' avoids 'ax-10' 'ax-11' 'ax-12'; $) + $} + $( A class abstraction defined by a negation. (Contributed by FL, 18-Sep-2010.) $) notab $p |- { x | -. ph } = ( _V \ { x | ph } ) $= @@ -39627,7 +39698,6 @@ technically classes despite morally (and provably) being sets, like ` 1 ` ${ $d x A $. $d x B $. - $( Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) $) dfrab3 $p |- { x e. A | ph } = ( A i^i { x | ph } ) $= @@ -40463,25 +40533,11 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets, PADBCQUGMKDRTUAUB $. $} - ${ - $d x y z $. $d A y $. $d A z $. - $( The proper substitution of a class into the empty set is the empty set. - (Contributed by NM, 18-Aug-2018.) Avoid ~ ax-12 . (Revised by Gino - Giotto, 28-Jun-2024.) $) - csb0 $p |- [_ A / x ]_ (/) = (/) $= - ( vy vz cvv wcel c0 csb wceq wnfc nfcv wa cv wsbc cab df-csb wnf wb wsb - wi dfsbcq2 bibi1d imbi2d sbv a1i vtoclg impel abbi1dv syl5eq mpan2 csbprc - nfcr pm2.61i ) BEFZABGHZGIZUNAGJZUPAGKUNUQLZUOCMGFZABNZCOGACBGPURUTCGUNUS - AQZUTUSRZUQVAUSADSZUSRZTVAVBTDBEDMBIZVDVBVAVEVCUTUSUSADBUAUBUCVDVAUSADUDU - EUFACGULUGUHUIUJABGUKUM $. - $( $j usage 'csb0' avoids 'ax-10' 'ax-11' 'ax-12'; $) - $} - - $( Obsolete version of ~ csb0 as of 28-Jun-2024. (Contributed by NM, - 18-Aug-2018.) (Proof modification is discouraged.) - (New usage is discouraged.) $) - csb0OLD $p |- [_ A / x ]_ (/) = (/) $= + $( The proper substitution of a class into the empty set is the empty set. + (Contributed by NM, 18-Aug-2018.) $) + csb0 $p |- [_ A / x ]_ (/) = (/) $= ( cvv wcel c0 csb wceq csbconstg csbprc pm2.61i ) BCDABEFEGABECHABEIJ $. + $( $j usage 'csb0' avoids 'ax-10' 'ax-11' 'ax-12'; $) ${ $d x y z $. $d y z A $. $d y z B $. $d y z C $. @@ -41639,7 +41695,7 @@ disjoint classes (see ~ disjdif ). Part of proof of Corollary 6K of $} ${ - $d x ph $. $d x A $. $d x B $. $d x C $. + $d x y ph $. $d x y A $. $d x y B $. $d x C $. $( An alternate definition of the conditional operator ~ df-if with one fewer connectives (but probably less intuitive to understand). (Contributed by NM, 30-Jan-2006.) $) @@ -41653,9 +41709,11 @@ fewer connectives (but probably less intuitive to understand). class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) $) dfif6 $p |- if ( ph , A , B ) = ( { x e. A | ph } u. { x e. B | -. ph } ) $= - ( cv wcel wa cab wn cun wo crab cif unab df-rab uneq12i df-if 3eqtr4ri ) - BEZCFAGZBHZSDFAIZGZBHZJTUCKBHABCLZUBBDLZJACDMTUCBNUEUAUFUDABCOUBBDOPABCDQ - R $. + ( vy cv wcel wa cab wn cun wo crab cif eleq1w anbi1d unabw df-rab uneq12i + weq df-if 3eqtr4ri ) BFZCGZAHZBIZUCDGZAJZHZBIZKEFZCGZAHZUKDGZUHHZLEIABCMZ + UHBDMZKACDNUEUIUMUOBEBETZUDULABECOPURUGUNUHBEDOPQUPUFUQUJABCRUHBDRSAECDUA + UB $. + $( $j usage 'dfif6' avoids 'ax-10' 'ax-11' 'ax-12'; $) $( Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) $) @@ -41737,7 +41795,7 @@ fewer connectives (but probably less intuitive to understand). $} ${ - $d y A $. $d y B $. $d x y ph $. + $d y A $. $d y B $. $d x y z ph $. dfif3.1 $e |- C = { x | ph } $. $( Alternate definition of the conditional operator ~ df-if . Note that ` ph ` is independent of ` x ` i.e. a constant true or false. @@ -41745,10 +41803,11 @@ fewer connectives (but probably less intuitive to understand). 8-Sep-2013.) $) dfif3 $p |- if ( ph , A , B ) = ( ( A i^i C ) u. ( B i^i ( _V \ C ) ) ) $= - ( vy cif crab wn cun cin cvv cdif dfif6 cab weq ineq2i dfrab3 eqtr4i - biidd cbvabv eqtri notab difeq2i eqtr2i uneq12i ) ACDHAGCIZAJZGDIZKCELZDM - ENZLZKAGCDOUKUHUMUJUKCAGPZLUHEUNCEABPUNFAABGBGQAUAUBUCZRAGCSTUJDUIGPZLUMU - IGDSUPULDUPMUNNULAGUDEUNMUOUETRUFUGT $. + ( vy vz crab cun cin cvv cdif cab weq biidd cbvabv eqtri ineq2i eqtr4i wn + cif dfif6 dfrab3 notabw difeq2i eqtr2i uneq12i ) ACDUBAGCIZAUAZGDIZJCEKZD + LEMZKZJAGCDUCULUIUNUKULCAGNZKUIEUOCEABNZUOFAABGBGOAPQRSAGCUDTUKDUJGNZKUNU + JGDUDUQUMDUQLAHNZMUMAAGHGHOAPUEEURLEUPURFAABHBHOAPQRUFTSUGUHT $. + $( $j usage 'dfif3' avoids 'ax-10' 'ax-11' 'ax-12'; $) $( Alternate definition of the conditional operator ~ df-if . Note that ` ph ` is independent of ` x ` i.e. a constant true or false. @@ -44831,39 +44890,20 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). ${ $d x A $. $d x B $. $d x C $. $( Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) - (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ~ ax-10 , ~ ax-11 , - ~ ax-12 . (Revised by Gino Giotto, 26-May-2024.) $) + (Revised by Mario Carneiro, 26-Apr-2015.) $) opeq1 $p |- ( A = B -> <. A , C >. = <. B , C >. ) $= - ( vx wceq cvv wcel cv csn cpr w3a cab cop eleq1 sneq preq1 preq12d eleq2d - 3anbi13d df-op abbidv 3eqtr4g ) ABEZAFGZCFGZDHZAIZACJZJZGZKZDLBFGZUEUFBIZ - BCJZJZGZKZDLACMBCMUCUKUQDUCUDULUJUPUEABFNUCUIUOUFUCUGUMUHUNABOABCPQRSUADA - CTDBCTUB $. - $( $j usage 'opeq1' avoids 'ax-10' 'ax-11' 'ax-12'; $) - - $( Obsolete version of ~ opeq1 as of 25-May-2024. (Contributed by NM, - 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) - (Proof modification is discouraged.) (New usage is discouraged.) $) - opeq1OLD $p |- ( A = B -> <. A , C >. = <. B , C >. ) $= ( wceq cvv wcel wa csn cpr c0 cif cop eleq1 anbi1d preq1 preq12d ifbieq1d sneq dfopif 3eqtr4g ) ABDZAEFZCEFZGZAHZACIZIZJKBEFZUCGZBHZBCIZIZJKACLBCLU AUDUIUGULJUAUBUHUCABEMNUAUEUJUFUKABRABCOPQACSBCST $. + $( $j usage 'opeq1' avoids 'ax-10' 'ax-11' 'ax-12'; $) $( Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) - (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ~ ax-10 , ~ ax-11 , - ~ ax-12 . (Revised by Gino Giotto, 26-May-2024.) $) + (Revised by Mario Carneiro, 26-Apr-2015.) $) opeq2 $p |- ( A = B -> <. C , A >. = <. C , B >. ) $= - ( vx wceq cvv wcel csn cpr w3a cab cop eleq1 preq2 preq2d eleq2d 3anbi23d - cv abbidv df-op 3eqtr4g ) ABEZCFGZAFGZDRZCHZCAIZIZGZJZDKUCBFGZUEUFCBIZIZG - ZJZDKCALCBLUBUJUODUBUDUKUIUNUCABFMUBUHUMUEUBUGULUFABCNOPQSDCATDCBTUA $. - $( $j usage 'opeq2' avoids 'ax-10' 'ax-11' 'ax-12'; $) - - $( Obsolete version of ~ opeq2 as of 25-May-2024. (Contributed by NM, - 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) - (Proof modification is discouraged.) (New usage is discouraged.) $) - opeq2OLD $p |- ( A = B -> <. C , A >. = <. C , B >. ) $= ( wceq cvv wcel wa csn cpr c0 cif cop eleq1 anbi2d preq2d ifbieq1d dfopif preq2 3eqtr4g ) ABDZCEFZAEFZGZCHZCAIZIZJKUABEFZGZUDCBIZIZJKCALCBLTUCUHUFU JJTUBUGUAABEMNTUEUIUDABCROPCAQCBQS $. + $( $j usage 'opeq2' avoids 'ax-10' 'ax-11' 'ax-12'; $) $} $( Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.) $) @@ -48185,12 +48225,26 @@ although the definition does not require it (see ~ dfid2 for a case $} ${ - $d x y z w $. $d z w ph $. $d x y ps $. + $d x y z w $. $d z w v ph $. $d x y v ps $. cbvopabv.1 $e |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) ) $. $( Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, - 15-Oct-1996.) $) + 15-Oct-1996.) Reduce axiom usage. (Revised by Gino Giotto, + 15-Oct-2024.) $) cbvopabv $p |- { <. x , y >. | ph } = { <. z , w >. | ps } $= + ( vv cv cop wceq wa wex cab copab weq opeq12 eqeq2d anbi12d df-opab abbii + cbvex2vw 3eqtr4i ) HIZCIZDIZJZKZALZDMCMZHNUDEIZFIZJZKZBLZFMEMZHNACDOBEFOU + JUPHUIUOCDEFCEPDFPLZUHUNABUQUGUMUDUEUFUKULQRGSUBUAACDHTBEFHTUC $. + $( $j usage 'cbvopabv' avoids 'ax-10' 'ax-11' 'ax-12'; $) + $} + + ${ + $d x y z w $. $d z w ph $. $d x y ps $. + cbvopabvOLD.1 $e |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) ) $. + $( Obsolete version of ~ cbvopabv as of 15-Oct-2024. (Contributed by NM, + 15-Oct-1996.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + cbvopabvOLD $p |- { <. x , y >. | ph } = { <. z , w >. | ps } $= ( nfv cbvopab ) ABCDEFAEHAFHBCHBDHGI $. $} @@ -48283,16 +48337,18 @@ although the definition does not require it (see ~ dfid2 for a case $} ${ - $d x z $. $d y z $. $d ph z $. $d ps z $. + $d x z w $. $d y z w $. $d ph z w $. $d ps z w $. $( Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) $) unopab $p |- ( { <. x , y >. | ph } u. { <. x , y >. | ps } ) = { <. x , y >. | ( ph \/ ps ) } $= - ( vz cv cop wceq wa wex cab wo copab unab 19.43 andi exbii bitr2i df-opab - cun bitr3i abbii eqtri uneq12i 3eqtr4i ) EFCFDFGHZAIZDJZCJZEKZUFBIZDJZCJZ - EKZTZUFABLZIZDJZCJZEKZACDMZBCDMZTUPCDMUOUIUMLZEKUTUIUMENVCUSEVCUHULLZCJUS - UHULCOVDURCURUGUKLZDJVDUQVEDUFABPQUGUKDORQUAUBUCVAUJVBUNACDESBCDESUDUPCDE - SUE $. + ( vz vw cv cop wa wex cab cun wo copab anbi1d 2exbidv 19.43 exbii df-opab + wceq weq eqeq1 unabw andi bitr2i bitr3i abbii eqtri uneq12i 3eqtr4i ) EGZ + CGDGHZTZAIZDJCJZEKZUMBIZDJCJZEKZLZFGZULTZABMZIZDJZCJZFKZACDNZBCDNZLVCCDNU + TVBAIZDJZCJZVBBIZDJZCJZMZFKVGUOURVLVOEFEFUAZUNVJCDVQUMVBAUKVAULUBZOPVQUQV + MCDVQUMVBBVROPUCVPVFFVPVKVNMZCJVFVKVNCQVSVECVEVJVMMZDJVSVDVTDVBABUDRVJVMD + QUERUFUGUHVHUPVIUSACDESBCDESUIVCCDFSUJ $. + $( $j usage 'unopab' avoids 'ax-10' 'ax-11' 'ax-12'; $) $}