Skip to content

Commit 34f3edb

Browse files
LegionMammal978LegionMammal978
committed
Shorten axpr and reduce axiom usage
1 parent c5147c2 commit 34f3edb

File tree

2 files changed

+171
-40
lines changed

2 files changed

+171
-40
lines changed

‎discouraged‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1731,6 +1731,9 @@
17311731
"axpowndlem2" is used by "axpowndlem3".
17321732
"axpowndlem3" is used by "axpowndlem4".
17331733
"axpowndlem4" is used by "axpownd".
1734+
"axprlem3OLD" is used by "axprOLD".
1735+
"axprlem4OLD" is used by "axprOLD".
1736+
"axprlem5OLD" is used by "axprOLD".
17341737
"axregnd" is used by "axregprim".
17351738
"axregnd" is used by "zfcndreg".
17361739
"axregndlem1" is used by "axregnd".
@@ -14947,14 +14950,20 @@ New usage of "axpowndlem3" is discouraged (1 uses).
1494714950
New usage of "axpowndlem4" is discouraged (1 uses).
1494814951
New usage of "axpr" is discouraged (0 uses).
1494914952
New usage of "axprALT" is discouraged (0 uses).
14953+
New usage of "axprOLD" is discouraged (0 uses).
1495014954
New usage of "axpre-ltadd" is discouraged (0 uses).
1495114955
New usage of "axpre-lttri" is discouraged (0 uses).
1495214956
New usage of "axpre-lttrn" is discouraged (0 uses).
1495314957
New usage of "axpre-mulgt0" is discouraged (0 uses).
1495414958
New usage of "axpre-sup" is discouraged (0 uses).
14959+
New usage of "axprlem3OLD" is discouraged (1 uses).
14960+
New usage of "axprlem4OLD" is discouraged (1 uses).
14961+
New usage of "axprlem5OLD" is discouraged (1 uses).
1495514962
New usage of "axregnd" is discouraged (2 uses).
1495614963
New usage of "axregndlem1" is discouraged (2 uses).
1495714964
New usage of "axregndlem2" is discouraged (1 uses).
14965+
New usage of "axrep4OLD" is discouraged (0 uses).
14966+
New usage of "axrep6OLD" is discouraged (0 uses).
1495814967
New usage of "axrepnd" is discouraged (2 uses).
1495914968
New usage of "axrepndlem1" is discouraged (1 uses).
1496014969
New usage of "axrepndlem2" is discouraged (1 uses).
@@ -15056,6 +15065,7 @@ New usage of "blof" is discouraged (5 uses).
1505615065
New usage of "bloln" is discouraged (6 uses).
1505715066
New usage of "blometi" is discouraged (1 uses).
1505815067
New usage of "bloval" is discouraged (2 uses).
15068+
New usage of "bm1.3iiOLD" is discouraged (0 uses).
1505915069
New usage of "bnj1000" is discouraged (1 uses).
1506015070
New usage of "bnj1001" is discouraged (1 uses).
1506115071
New usage of "bnj1006" is discouraged (1 uses).
@@ -20066,6 +20076,12 @@ Proof modification of "axnul" is discouraged (36 steps).
2006620076
Proof modification of "axnulALT" is discouraged (95 steps).
2006720077
Proof modification of "axnulALT2" is discouraged (57 steps).
2006820078
Proof modification of "axprALT" is discouraged (67 steps).
20079+
Proof modification of "axprOLD" is discouraged (122 steps).
20080+
Proof modification of "axprlem3OLD" is discouraged (152 steps).
20081+
Proof modification of "axprlem4OLD" is discouraged (149 steps).
20082+
Proof modification of "axprlem5OLD" is discouraged (132 steps).
20083+
Proof modification of "axrep4OLD" is discouraged (130 steps).
20084+
Proof modification of "axrep6OLD" is discouraged (113 steps).
2006920085
Proof modification of "axsepg2ALT" is discouraged (170 steps).
2007020086
Proof modification of "barbariALT" is discouraged (22 steps).
2007120087
Proof modification of "barocoALT" is discouraged (24 steps).
@@ -20316,6 +20332,7 @@ Proof modification of "bj-xpima1snALT" is discouraged (25 steps).
2031620332
Proof modification of "bj-xpima2sn" is discouraged (23 steps).
2031720333
Proof modification of "bj-xpnzex" is discouraged (71 steps).
2031820334
Proof modification of "bj-zfauscl" is discouraged (65 steps).
20335+
Proof modification of "bm1.3iiOLD" is discouraged (95 steps).
2031920336
Proof modification of "brdomgOLD" is discouraged (118 steps).
2032020337
Proof modification of "brdomiOLD" is discouraged (30 steps).
2032120338
Proof modification of "brenOLD" is discouraged (130 steps).

‎set.mm‎

Lines changed: 154 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -50480,12 +50480,39 @@ under a function is also a set (see the variant ~ funimaex ). Although
5048050480
$}
5048150481

5048250482
${
50483-
$d x y z w $.
50483+
$d z ph $. $d w x y z $.
50484+
$( Version of ~ axrep4 with a disjoint variable condition, requiring fewer
50485+
axioms. (Contributed by Matthew House, 18-Sep-2025.) $)
50486+
axrep4v $p |- ( A. x E. z A. y ( ph -> y = z ) ->
50487+
E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) ) $=
50488+
( wal weq wi wex wel wa wb ax-rep 19.3v imbi1i albii exbii anbi2i 3imtr3i
50489+
bibi2i ) ADFZCDGZHZCFZDIZBFCDJZBEJZUAKZBIZLZCFZDIAUBHZCFZDIZBFUFUGAKZBIZL
50490+
ZCFZDIAEDCBMUEUNBUDUMDUCULCUAAUBADNZOPQPUKURDUJUQCUIUPUFUHUOBUAAUGUSRQTPQ
50491+
S $.
50492+
$( $j usage 'axrep4v' avoids 'ax-12'; $)
50493+
$}
50494+
50495+
${
50496+
$d w x y z $.
5048450497
axrep4.1 $e |- F/ z ph $.
5048550498
$( A more traditional version of the Axiom of Replacement. (Contributed by
50486-
NM, 14-Aug-1994.) $)
50499+
NM, 14-Aug-1994.) (Proof shortened by Matthew House, 18-Sep-2025.) $)
5048750500
axrep4 $p |- ( A. x E. z A. y ( ph -> y = z ) ->
5048850501
E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) ) $=
50502+
( wal weq wi wex wel wa wb ax-rep 19.3 imbi1i albii exbii anbi2i bibi2i
50503+
3imtr3i ) ADGZCDHZIZCGZDJZBGCDKZBEKZUBLZBJZMZCGZDJAUCIZCGZDJZBGUGUHALZBJZ
50504+
MZCGZDJAEDCBNUFUOBUEUNDUDUMCUBAUCADFOZPQRQULUSDUKURCUJUQUGUIUPBUBAUHUTSRT
50505+
QRUA $.
50506+
$}
50507+
50508+
${
50509+
$d x y z w $.
50510+
axrep4OLD.1 $e |- F/ z ph $.
50511+
$( Obsolete version of ~ axrep4 as of 18-Sep-2025. (Contributed by NM,
50512+
14-Aug-1994.) (Proof modification is discouraged.)
50513+
(New usage is discouraged.) $)
50514+
axrep4OLD $p |- ( A. x E. z A. y ( ph -> y = z ) ->
50515+
E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) ) $=
5048950516
( weq wi wal wex wel wa wb axrep3 19.35i nfv nfa1 nfan nfbi nfal nfex a1i
5049050517
nfe1 elequ2 19.3 anbi2i exbii bibi12d albidv cbvexv1 sylib ) ACDGHCIDJZBI
5049150518
CBKZBEKZADIZLZBJZMZCIZBJCDKZUNALZBJZMZCIZDJULUSBABDCENOUSVDBDURDCUMUQDUMD
@@ -50515,8 +50542,21 @@ under a function is also a set (see the variant ~ funimaex ). Although
5051550542

5051650543
${
5051750544
$d w x y z $. $d y ph $.
50518-
$( A condensed form of ~ ax-rep . (Contributed by SN, 18-Sep-2023.) $)
50545+
$( A condensed form of ~ ax-rep . (Contributed by SN, 18-Sep-2023.)
50546+
(Proof shortened by Matthew House, 18-Sep-2025.) $)
5051950547
axrep6 $p |- ( A. w E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) ) $=
50548+
( weq wi wal wex wel wa wb wmo cv wrex axrep4v df-mo albii df-rex bibi2i
50549+
exbii 3imtr4i ) ADCFGDHCIZEHDCJZEBJAKEIZLZDHZCIADMZEHUDAEBNZOZLZDHZCIAEDC
50550+
BPUHUCEADCQRULUGCUKUFDUJUEUDAEUISTRUAUB $.
50551+
$}
50552+
50553+
${
50554+
$d w x y z $. $d y ph $.
50555+
$( Obsolete version of ~ axrep6 as of 18-Sep-2025. (Contributed by SN,
50556+
18-Sep-2023.) (Proof modification is discouraged.)
50557+
(New usage is discouraged.) $)
50558+
axrep6OLD $p |- ( A. w E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) )
50559+
$=
5052050560
( wal weq wi wex wel wa wb wmo cv wrex ax-rep df-mo 19.3v albii exbii
5052150561
imbi1i bitr4i rexbii df-rex bitr3i bibi2i 3imtr4i ) ACFZDCGZHZDFZCIZEFDCJ
5052250562
ZEBJUHKEIZLZDFZCIADMZEFUMAEBNZOZLZDFZCIABCDEPUQULEUQAUIHZDFZCIULADCQUKVCC
@@ -50686,12 +50726,35 @@ under a function is also a set (see the variant ~ funimaex ). Although
5068650726
$}
5068750727

5068850728
${
50689-
$d x ph z $. $d x y z $.
50729+
$d x y z $. $d x y ph $.
50730+
bm1.3iiv.1 $e |- E. x A. z ( ph -> z e. x ) $.
50731+
$( Version of ~ bm1.3ii combined with a change of variable, requiring fewer
50732+
axioms. (Contributed by Matthew House, 18-Sep-2025.) $)
50733+
bm1.3iiv $p |- E. y A. z ( z e. y <-> ph ) $=
50734+
( wel wi wal wb wex wa ax-sep bimsc1 ex al2imi eximdv mpi exlimiiv ) ADBF
50735+
ZGZDHZDCFZAIZDHZCJZBUAUBSAKIZDHZCJUEADCBLUAUGUDCTUFUCDTUFUCASUBMNOPQER $.
50736+
$( $j usage 'bm1.3iiv' avoids 'ax-9' 'ax-12'; $)
50737+
$}
50738+
50739+
${
50740+
$d x y z $. $d x z ph $.
5069050741
bm1.3ii.1 $e |- E. x A. y ( ph -> y e. x ) $.
5069150742
$( Convert implication to equivalence using the Separation Scheme
5069250743
(Aussonderung) ~ ax-sep . Similar to Theorem 1.3(ii) of [BellMachover]
50693-
p. 463. (Contributed by NM, 21-Jun-1993.) $)
50744+
p. 463. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Matthew
50745+
House, 18-Sep-2025.) $)
5069450746
bm1.3ii $p |- E. x A. y ( y e. x <-> ph ) $=
50747+
( vz wel wi wal wex weq elequ2 imbi2d albidv cbvexvw mpbi bm1.3iiv ) AEBC
50748+
ACBFZGZCHZBIACEFZGZCHZEIDSUBBEBEJZRUACUCQTABECKLMNOP $.
50749+
$}
50750+
50751+
${
50752+
$d x ph z $. $d x y z $.
50753+
bm1.3iiOLD.1 $e |- E. x A. y ( ph -> y e. x ) $.
50754+
$( Obsolete version of ~ bm1.3ii as of 18-Sep-2025. (Contributed by NM,
50755+
21-Jun-1993.) (Proof modification is discouraged.)
50756+
(New usage is discouraged.) $)
50757+
bm1.3iiOLD $p |- E. x A. y ( y e. x <-> ph ) $=
5069550758
( vz wel wi wal wa wb wex 19.42v bimsc1 eximi sylbir elequ2 imbi2d albidv
5069650759
alanimi weq cbvexvw mpbi ax-sep exan exlimiiv ) ACEFZGZCHZCBFZUFAIJZCHZBK
5069750760
ZIZUIAJZCHZBKZEUMUHUKIZBKUPUHUKBLUQUOBUGUJUNCAUFUIMSNOUHULEAUIGZCHZBKUHEK
@@ -52034,7 +52097,7 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with
5203452097
( vw wel wn wal wex ax-pow pm2.21 alimi a1i imim1d alimdv eximdv exlimiiv
5203552098
wi mpi ax-nul ) CDEZFCGZCBEZFZCGZBAEZQZBGZAHZDUAUBTQZCGZUEQZBGZAHUHDABCIU
5203652099
AULUGAUAUKUFBUAUDUJUEUDUJQUAUCUICUBTJKLMNORDCSP $.
52037-
$( $j usage 'axprlem1' avoids 'ax-ext' 'ax-sep'; $)
52100+
$( $j usage 'axprlem1' avoids 'ax-8' 'ax-9' 'ax-12' 'ax-ext' 'ax-sep'; $)
5203852101
$}
5203952102

5204052103
${
@@ -52047,78 +52110,129 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with
5204752110
alimdv eximdv mpi axprlem1 exlimiiv ) DCFGDHZCEFZIZCHZUDCBJZKZBAFZIZBHZAL
5204852111
ZEUGCBFZUEIZCHZUJIZBHZALUMEABCMUGURULAUGUQUKBUGUIUPUJUIUNUDIZCHUGUPUDCUHN
5204952112
UFUSUOCUDUEUNOPQRSTUAECDUBUC $.
52050-
$( $j usage 'axprlem2' avoids 'ax-ext' 'ax-sep'; $)
52113+
$( $j usage 'axprlem2' avoids 'ax-8' 'ax-9' 'ax-12' 'ax-ext' 'ax-sep'; $)
5205152114
$}
5205252115

5205352116
${
5205452117
$d x z w $. $d y z w $. $d z w n $. $d z w s p $.
5205552118
$( Lemma for ~ axpr . Eliminate the antecedent of the relevant replacement
52056-
instance. (Contributed by Rohan Ridenour, 10-Aug-2023.) $)
52119+
instance. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Proof
52120+
shortened by Matthew House, 18-Sep-2025.) $)
5205752121
axprlem3 $p |- E. z A. w ( w e. z <->
5205852122
E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $=
52123+
( wel wex weq wif wi wal wa wb biimpd equeuclr syl9r alrimdv spimevw mpg
52124+
axrep4v ifptru wn ifpfal pm2.61i ) EFHEIZDAJZDBJZKZDCJZLZDMZCIZDCHFGHUJNF
52125+
IODMCIFUJFDCGUBUGUNUGUMCACAJZUGULDUGUJUHUOUKUGUJUHUGUHUIUCPCDAQRSTUGUDZUM
52126+
CBCBJZUPULDUPUJUIUQUKUPUJUIUGUHUIUEPCDBQRSTUFUA $.
52127+
$( $j usage 'axprlem3' avoids 'ax-8' 'ax-9' 'ax-12' 'ax-ext'; $)
52128+
$}
52129+
52130+
${
52131+
$d w s $. $d v s $.
52132+
axprlem4.1 $e |- E. s A. n ph $.
52133+
axprlem4.2 $e |- ( ph -> ( n e. s -> A. t -. t e. n ) ) $.
52134+
axprlem4.3 $e |- ( A. n ph ->
52135+
( if- ( E. n n e. s , w = x , w = y ) <-> w = v ) ) $.
52136+
$( Lemma for ~ axpr . If an existing set of empty sets corresponds to one
52137+
element of the pair, then the element is included in any superset of the
52138+
set whose existence is asserted by the axiom of replacement.
52139+
(Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ,
52140+
13-Aug-2023.) (Revised by Matthew House, 18-Sep-2025.) $)
52141+
axprlem4 $p |- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( w = v ->
52142+
E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) ) $=
52143+
( wel wn wal cv wi wa wex weq wral wif alimi df-ral sylibr imim1i aleximi
52144+
ancrd mpi biimprcd anim2d eximdv syl5com ) FGMNFOZGHPZUAZHIMZQZHOZUQAGOZR
52145+
ZHSZDETZUQGHMZGSDBTDCTUBZRZHSUSUTHSVBJURUTVAHURUTUQUTUPUQUTVDUNQZGOUPAVGG
52146+
KUCUNGUOUDUEUFUHUGUIVCVAVFHVCUTVEUQUTVEVCLUJUKULUM $.
52147+
$( $j usage 'axprlem4' avoids 'ax-8' 'ax-9' 'ax-12' 'ax-ext'; $)
52148+
$}
52149+
52150+
${
52151+
$d x z w s p $. $d y z w s p $. $d z w t n s p $.
52152+
$( Unabbreviated version of the Axiom of Pairing of ZF set theory, derived
52153+
as a theorem from the other axioms.
52154+
52155+
This theorem should not be referenced by any proof. Instead, use
52156+
~ ax-pr below so that the uses of the Axiom of Pairing can be more
52157+
easily identified.
52158+
52159+
For a shorter proof using ~ ax-ext , see ~ axprALT . (Contributed by
52160+
NM, 14-Nov-2006.) Remove dependency on ~ ax-ext . (Revised by Rohan
52161+
Ridenour, 10-Aug-2023.) (Proof shortened by BJ, 13-Aug-2023.) (Proof
52162+
shortened by Matthew House, 18-Sep-2025.) Use ~ ax-pr instead.
52163+
(New usage is discouraged.) $)
52164+
axpr $p |- E. z A. w ( ( w = x \/ w = y ) -> w e. z ) $=
52165+
( vt vn vs vp wel wn wal cv wral wi weq wo wex wb ax-nul axprlem4 wa exbi
52166+
wif axprlem3 axprlem1 bm1.3iiv biimp mpbiri ifptru syl pm2.21 alnex sylbi
52167+
ifpfal jaod imbi2 syl5ibrcom alimdv eximdv mpi axprlem2 exlimiiv ) EFIJEK
52168+
ZFGLMGHIZNGKZDAOZDBOZPZDCIZNZDKZCQZHVEVIVDFGIZFQZVFVGUCZUAGQZRZDKZCQVLABC
52169+
DFGHUDVEVRVKCVEVQVJDVEVJVQVHVPNVEVFVPVGVMVCRZABDAEFGHVCCGFCFEUEUFVMVCUGVS
52170+
FKZVNVOVFRVTVNVCFQFESVMVCFUBUHVNVFVGUIUJTVMJZABDBEFGHGFSVMVCUKWAFKVNJVOVG
52171+
RVMFULVNVFVGUNUMTUOVIVPVHUPUQURUSUTHGFEVAVB $.
52172+
$( $j usage 'axpr' avoids 'ax-8' 'ax-9' 'ax-10' 'ax-11' 'ax-12'
52173+
'ax-ext'; $)
52174+
$}
52175+
52176+
${
52177+
$d x z w $. $d y z w $. $d z w n $. $d z w s p $.
52178+
$( Obsolete version of ~ axprlem3 as of 18-Sep-2025. (Contributed by Rohan
52179+
Ridenour, 10-Aug-2023.) (Proof modification is discouraged.)
52180+
(New usage is discouraged.) $)
52181+
axprlem3OLD $p |- E. z A. w ( w e. z <->
52182+
E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $=
5205952183
( cv wcel wex weq wi wal wa ax6evr biimpd alrimiv expcom eximdv mpi wb wn
5206052184
wif axrep4 ifptru equtrr sylan9r ifpfal adantl simpl equtr syl6ci pm2.61i
5206152185
nfv mpg ) EHFHZIEJZDAKZDBKZUCZDCKZLZDMZCJZDHCHIUPGHIUTNFJUADMCJFUTFDCGUTC
5206252186
UNUDUQVDUQACKZCJVDCAOUQVEVCCVEUQVCVEUQNVBDUQUTURVEVAUQUTURUQURUSUEPACDUFU
5206352187
GQRSTUQUBZBCKZCJVDCBOVFVGVCCVGVFVCVGVFNZVBDVHUTUSVGVAVFUTUSLVGVFUTUSUQURU
5206452188
SUHPUIVGVFUJDBCUKULQRSTUMUO $.
52065-
$( $j usage 'axprlem3' avoids 'ax-ext'; $)
52189+
$( $j usage 'axprlem3OLD' avoids 'ax-ext'; $)
5206652190
$}
5206752191

5206852192
${
5206952193
$d x s $. $d w s $. $d t n s $.
52070-
$( Lemma for ~ axpr . The first element of the pair is included in any
52071-
superset of the set whose existence is asserted by the axiom of
52072-
replacement. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by
52073-
BJ, 13-Aug-2023.) $)
52074-
axprlem4 $p |- ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = x )
52075-
-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $=
52194+
$( Obsolete version of ~ axprlem4 as of 18-Sep-2025. (Contributed by Rohan
52195+
Ridenour, 10-Aug-2023.) (Proof modification is discouraged.)
52196+
(New usage is discouraged.) $)
52197+
axprlem4OLD $p |- ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p )
52198+
/\ w = x ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $=
5207652199
( wel wn wal cv wral wi weq wa wex nfa1 sp eximd mpi wif axprlem1 bm1.3ii
5207752200
wb nfv nfan biimp alimi df-ral sylibr mpan9 adantrr ax-nul biimprd simprr
5207852201
ifptru biimpar syl2an2r jca expcom ) DEHIDJZEFKZLZFGHZMZFJZCANZOZEFHZVAUD
5207952202
ZEJZFPVDVIEPZVGCBNZUAZOZFPVAFEFEDUBUCVHVKVOFVFVGFVEFQVGFUEUFVKVHVOVKVHOVD
5208052203
VNVKVFVDVGVKVCVFVDVKVIVAMZEJVCVJVPEVIVAUGUHVAEVBUIUJVEFRUKULVKVLVHVGVNVKV
5208152204
AEPVLEDUMVKVAVIEVJEQVKVIVAVJERUNSTVKVFVGUOVLVNVGVLVGVMUPUQURUSUTST $.
52082-
$( $j usage 'axprlem4' avoids 'ax-ext'; $)
52205+
$( $j usage 'axprlem4OLD' avoids 'ax-ext'; $)
5208352206
$}
5208452207

5208552208
${
5208652209
$d y s $. $d w s $. $d n s $.
52087-
$( Lemma for ~ axpr . The second element of the pair is included in any
52088-
superset of the set whose existence is asserted by the axiom of
52089-
replacement. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by
52090-
BJ, 13-Aug-2023.) $)
52091-
axprlem5 $p |- ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y )
52092-
-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $=
52210+
$( Obsolete version of ~ axprlem4 as of 18-Sep-2025. (Contributed by Rohan
52211+
Ridenour, 10-Aug-2023.) (Proof modification is discouraged.)
52212+
(New usage is discouraged.) $)
52213+
axprlem5OLD $p |- ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p )
52214+
/\ w = y ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $=
5209352215
( wel wn wal cv wral wi weq wa wex wif ax-nul nfa1 nfv nfan pm2.21 adantr
5209452216
alimi df-ral sylibr ad2antrl mpd simpl alnex sylib simprr biimpar syl2anc
5209552217
sp ifpfal jca expcom eximd mpi ) DEHIDJZEFKZLZFGHZMZFJZCBNZOZEFHZIZEJZFPV
5209652218
DVIEPZCANZVGQZOZFPFERVHVKVOFVFVGFVEFSVGFTUAVKVHVOVKVHOZVDVNVPVCVDVPVIVAMZ
5209752219
EJZVCVKVRVHVJVQEVIVAUBUDUCVAEVBUEUFVFVEVKVGVEFUOUGUHVPVLIZVGVNVPVKVSVKVHU
5209852220
IVIEUJUKVKVFVGULVSVNVGVLVMVGUPUMUNUQURUSUT $.
52099-
$( $j usage 'axprlem5' avoids 'ax-ext'; $)
52221+
$( $j usage 'axprlem5OLD' avoids 'ax-ext'; $)
5210052222
$}
5210152223

5210252224
${
5210352225
$d x z w s p $. $d y z w s p $. $d z w t n s p $.
52104-
$( Unabbreviated version of the Axiom of Pairing of ZF set theory, derived
52105-
as a theorem from the other axioms.
52106-
52107-
This theorem should not be referenced by any proof. Instead, use
52108-
~ ax-pr below so that the uses of the Axiom of Pairing can be more
52109-
easily identified.
52110-
52111-
For a shorter proof using ~ ax-ext , see ~ axprALT . (Contributed by
52112-
NM, 14-Nov-2006.) Remove dependency on ~ ax-ext . (Revised by Rohan
52113-
Ridenour, 10-Aug-2023.) (Proof shortened by BJ, 13-Aug-2023.) Use
52114-
~ ax-pr instead. (New usage is discouraged.) $)
52115-
axpr $p |- E. z A. w ( ( w = x \/ w = y ) -> w e. z ) $=
52226+
$( Obsolete version of ~ axpr as of 18-Sep-2025. (Contributed by NM,
52227+
14-Nov-2006.) (Proof modification is discouraged.)
52228+
(New usage is discouraged.) $)
52229+
axprOLD $p |- E. z A. w ( ( w = x \/ w = y ) -> w e. z ) $=
5211652230
( vt vn vs vp wel wn wal cv wral wi weq wo wex wif wa wb biimpr eximii ex
52117-
axprlem3 alimi axprlem4 axprlem5 jaodan imim1d alimdv eximdv mpi axprlem2
52118-
exlimiiv ) EFIJEKFGLMGHIZNGKZDAOZDBOZPZDCIZNZDKZCQZHUPUOFGIFQUQURRSGQZUTN
52119-
ZDKZCQVCUTVDTZDKVFCABCDFGHUDVGVEDUTVDUAUEUBUPVFVBCUPVEVADUPUSVDUTUPUSVDUP
52120-
UQVDURABDEFGHUFABDEFGHUGUHUCUIUJUKULHGFEUMUN $.
52121-
$( $j usage 'axpr' avoids 'ax-ext'; $)
52231+
axprlem3OLD alimi axprlem4OLD axprlem5OLD jaodan imim1d alimdv eximdv mpi
52232+
axprlem2 exlimiiv ) EFIJEKFGLMGHIZNGKZDAOZDBOZPZDCIZNZDKZCQZHUPUOFGIFQUQU
52233+
RRSGQZUTNZDKZCQVCUTVDTZDKVFCABCDFGHUDVGVEDUTVDUAUEUBUPVFVBCUPVEVADUPUSVDU
52234+
TUPUSVDUPUQVDURABDEFGHUFABDEFGHUGUHUCUIUJUKULHGFEUMUN $.
52235+
$( $j usage 'axprOLD' avoids 'ax-ext'; $)
5212252236
$}
5212352237

5212452238
${

0 commit comments

Comments
 (0)