From 39d4ac8750f6e46058820925991d8a265af408d9 Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sat, 8 Mar 2025 11:05:56 +0100 Subject: [PATCH 1/7] shorten cbvralsvw --- set.mm | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/set.mm b/set.mm index a4cf9f2c33..4cde6dd945 100644 --- a/set.mm +++ b/set.mm @@ -30714,8 +30714,15 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is $( Change bound variable by using a substitution. Version of ~ cbvralsv with a disjoint variable condition, which does not require ~ ax-13 . (Contributed by NM, 20-Nov-2005.) Avoid ~ ax-13 . (Revised by Gino - Giotto, 10-Jan-2024.) $) + Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 8-Mar-2025.) $) cbvralsvw $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $= + ( wsb nfv nfs1v sbequ12 cbvralw ) AABCEBCDACFABCGABCHI $. + + $( Obsolete version of ~ cbvralsvw as of 8-Mar-2025. (Contributed by NM, + 20-Nov-2005.) Avoid ~ ax-13. (Revised by Gino Giotto, 10-Jan-2024.) + (Proof modification is discouraged.) (New usage is discouraged.) + (Contributed by ?who?, 8-Mar-2025.) $) + cbvralsvwOLD $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $= ( vz wral wsb nfv nfs1v sbequ12 cbvralw sbequ bitri ) ABDFABEGZEDFABCGZCD FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $. $( $j usage 'cbvralsvw' avoids 'ax-13'; $) From 00d0fcf8ac95c5c730f3d0c3e1cc924a4ab2e5ad Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sat, 8 Mar 2025 11:23:16 +0100 Subject: [PATCH 2/7] shorten cbvresvw --- set.mm | 31 ++++++++++++++++++------------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/set.mm b/set.mm index 4cde6dd945..818a8023fc 100644 --- a/set.mm +++ b/set.mm @@ -30710,34 +30710,39 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is $} ${ - $d z x A $. $d y A $. $d z y ph $. $d x y $. + $d x y A $. $d y ph $. $( Change bound variable by using a substitution. Version of ~ cbvralsv with a disjoint variable condition, which does not require ~ ax-13 . (Contributed by NM, 20-Nov-2005.) Avoid ~ ax-13 . (Revised by Gino Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 8-Mar-2025.) $) cbvralsvw $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $= ( wsb nfv nfs1v sbequ12 cbvralw ) AABCEBCDACFABCGABCHI $. - - $( Obsolete version of ~ cbvralsvw as of 8-Mar-2025. (Contributed by NM, - 20-Nov-2005.) Avoid ~ ax-13. (Revised by Gino Giotto, 10-Jan-2024.) - (Proof modification is discouraged.) (New usage is discouraged.) - (Contributed by ?who?, 8-Mar-2025.) $) - cbvralsvwOLD $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $= - ( vz wral wsb nfv nfs1v sbequ12 cbvralw sbequ bitri ) ABDFABEGZEDFABCGZCD - FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $. $( $j usage 'cbvralsvw' avoids 'ax-13'; $) - $} - ${ - $d z x A $. $d y z ph $. $d y A $. $d x y $. $( Change bound variable by using a substitution. Version of ~ cbvrexsv with a disjoint variable condition, which does not require ~ ax-13 . (Contributed by NM, 2-Mar-2008.) Avoid ~ ax-13 . (Revised by Gino Giotto, 10-Jan-2024.) $) cbvrexsvw $p |- ( E. x e. A ph <-> E. y e. A [ y / x ] ph ) $= + ( wsb nfv nfs1v sbequ12 cbvrexw ) AABCEBCDACFABCGABCHI $. + $( $j usage 'cbvrexsvw' avoids 'ax-13'; $) + $} + + ${ + $d z x A $. $d y A $. $d z y ph $. $d x y $. + $( Obsolete version of ~ cbvralsvw as of 8-Mar-2025. (Contributed by NM, + 20-Nov-2005.) Avoid ~ ax-13. (Revised by Gino Giotto, 10-Jan-2024.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + cbvralsvwOLD $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $= + ( vz wral wsb nfv nfs1v sbequ12 cbvralw sbequ bitri ) ABDFABEGZEDFABCGZCD + FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $. + + $( Obsolete version of ~ cbvrexsvw as of 8-Mar-2025. (Contributed by NM, + 20-Nov-2005.) Avoid ~ ax-13. (Revised by Gino Giotto, 10-Jan-2024.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + cbvrexsvwOLD $p |- ( E. x e. A ph <-> E. y e. A [ y / x ] ph ) $= ( vz wrex wsb nfv nfs1v sbequ12 cbvrexw sbequ bitri ) ABDFABEGZEDFABCGZCD FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $. - $( $j usage 'cbvrexsvw' avoids 'ax-13'; $) $} ${ From 0ab23c3977439e104ac0a9da2065666092e9ece4 Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sat, 8 Mar 2025 11:24:48 +0100 Subject: [PATCH 3/7] add tag --- set.mm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/set.mm b/set.mm index 818a8023fc..87ddc6775d 100644 --- a/set.mm +++ b/set.mm @@ -30722,7 +30722,7 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is $( Change bound variable by using a substitution. Version of ~ cbvrexsv with a disjoint variable condition, which does not require ~ ax-13 . (Contributed by NM, 2-Mar-2008.) Avoid ~ ax-13 . (Revised by Gino - Giotto, 10-Jan-2024.) $) + Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 8-Mar-2025.) $) cbvrexsvw $p |- ( E. x e. A ph <-> E. y e. A [ y / x ] ph ) $= ( wsb nfv nfs1v sbequ12 cbvrexw ) AABCEBCDACFABCGABCHI $. $( $j usage 'cbvrexsvw' avoids 'ax-13'; $) From f32ec51253c5b34214c3bfc3e3e8867d3bfbb494 Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sat, 8 Mar 2025 11:28:07 +0100 Subject: [PATCH 4/7] typos --- set.mm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/set.mm b/set.mm index 87ddc6775d..393c847b39 100644 --- a/set.mm +++ b/set.mm @@ -30731,14 +30731,14 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ${ $d z x A $. $d y A $. $d z y ph $. $d x y $. $( Obsolete version of ~ cbvralsvw as of 8-Mar-2025. (Contributed by NM, - 20-Nov-2005.) Avoid ~ ax-13. (Revised by Gino Giotto, 10-Jan-2024.) + 20-Nov-2005.) Avoid ~ ax-13 . (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) $) cbvralsvwOLD $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $= ( vz wral wsb nfv nfs1v sbequ12 cbvralw sbequ bitri ) ABDFABEGZEDFABCGZCD FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $. $( Obsolete version of ~ cbvrexsvw as of 8-Mar-2025. (Contributed by NM, - 20-Nov-2005.) Avoid ~ ax-13. (Revised by Gino Giotto, 10-Jan-2024.) + 20-Nov-2005.) Avoid ~ ax-13 . (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) $) cbvrexsvwOLD $p |- ( E. x e. A ph <-> E. y e. A [ y / x ] ph ) $= ( vz wrex wsb nfv nfs1v sbequ12 cbvrexw sbequ bitri ) ABDFABEGZEDFABCGZCD From f30a80424afcf85e8424c07e3790399c611bf47b Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sat, 8 Mar 2025 11:30:32 +0100 Subject: [PATCH 5/7] discouraged --- discouraged | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/discouraged b/discouraged index 5356ef300c..c4c974b9e8 100644 --- a/discouraged +++ b/discouraged @@ -15362,6 +15362,7 @@ New usage of "cbvralcsf" is discouraged (2 uses). New usage of "cbvralf" is discouraged (2 uses). New usage of "cbvralfwOLD" is discouraged (0 uses). New usage of "cbvralsv" is discouraged (0 uses). +New usage of "cbvralsvwOLD" is discouraged (0 uses). New usage of "cbvralv" is discouraged (2 uses). New usage of "cbvralv2" is discouraged (1 uses). New usage of "cbvreu" is discouraged (2 uses). @@ -15375,6 +15376,7 @@ New usage of "cbvrexcsf" is discouraged (1 uses). New usage of "cbvrexdva2OLD" is discouraged (0 uses). New usage of "cbvrexf" is discouraged (1 uses). New usage of "cbvrexsv" is discouraged (1 uses). +New usage of "cbvrexsvwOLD" is discouraged (0 uses). New usage of "cbvrexv" is discouraged (2 uses). New usage of "cbvrexv2" is discouraged (0 uses). New usage of "cbvriota" is discouraged (1 uses). @@ -20109,9 +20111,11 @@ Proof modification of "cbvmptvOLD" is discouraged (13 steps). Proof modification of "cbvopab1vOLD" is discouraged (13 steps). Proof modification of "cbvopabvOLD" is discouraged (20 steps). Proof modification of "cbvralfwOLD" is discouraged (139 steps). +Proof modification of "cbvralsvwOLD" is discouraged (53 steps). Proof modification of "cbvreuvwOLD" is discouraged (13 steps). Proof modification of "cbvreuwOLD" is discouraged (145 steps). Proof modification of "cbvrexdva2OLD" is discouraged (109 steps). +Proof modification of "cbvrexsvwOLD" is discouraged (53 steps). Proof modification of "cbvriotavwOLD" is discouraged (13 steps). Proof modification of "cbvrmowOLD" is discouraged (58 steps). Proof modification of "ccat2s1fvwALT" is discouraged (116 steps). From 96817f5cb01e9805fc36fafa5fd4fc89fe403153 Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sat, 8 Mar 2025 14:39:25 +0100 Subject: [PATCH 6/7] revise raleq and friends --- discouraged | 8 +++ set.mm | 137 +++++++++++++++++++++++++++++++++------------------- 2 files changed, 94 insertions(+), 51 deletions(-) diff --git a/discouraged b/discouraged index c4c974b9e8..2c3dedf5f0 100644 --- a/discouraged +++ b/discouraged @@ -18755,6 +18755,8 @@ New usage of "ralcom2" is discouraged (0 uses). New usage of "ralcom3OLD" is discouraged (0 uses). New usage of "ralcom4OLD" is discouraged (0 uses). New usage of "raleleqALT" is discouraged (0 uses). +New usage of "raleqOLD" is discouraged (0 uses). +New usage of "raleqbidvvOLD" is discouraged (0 uses). New usage of "ralf0OLD" is discouraged (0 uses). New usage of "ralidmOLD" is discouraged (0 uses). New usage of "ralprgOLD" is discouraged (0 uses). @@ -18842,6 +18844,8 @@ New usage of "rexbidvALT" is discouraged (0 uses). New usage of "rexbidvaALT" is discouraged (0 uses). New usage of "rexcomOLD" is discouraged (0 uses). New usage of "rexdif1enOLD" is discouraged (0 uses). +New usage of "rexeqOLD" is discouraged (0 uses). +New usage of "rexeqbidvvOLD" is discouraged (0 uses). New usage of "reximdvaiOLD" is discouraged (0 uses). New usage of "reximiaOLD" is discouraged (0 uses). New usage of "rexlimddvcbv" is discouraged (0 uses). @@ -21190,6 +21194,8 @@ Proof modification of "ralcom13OLD" is discouraged (58 steps). Proof modification of "ralcom3OLD" is discouraged (38 steps). Proof modification of "ralcom4OLD" is discouraged (63 steps). Proof modification of "raleleqALT" is discouraged (26 steps). +Proof modification of "raleqOLD" is discouraged (11 steps). +Proof modification of "raleqbidvvOLD" is discouraged (98 steps). Proof modification of "ralf0OLD" is discouraged (41 steps). Proof modification of "ralidmOLD" is discouraged (68 steps). Proof modification of "ralprgOLD" is discouraged (17 steps). @@ -21258,6 +21264,8 @@ Proof modification of "rexbidvALT" is discouraged (10 steps). Proof modification of "rexbidvaALT" is discouraged (10 steps). Proof modification of "rexcomOLD" is discouraged (67 steps). Proof modification of "rexdif1enOLD" is discouraged (120 steps). +Proof modification of "rexeqOLD" is discouraged (11 steps). +Proof modification of "rexeqbidvvOLD" is discouraged (47 steps). Proof modification of "reximdvaiOLD" is discouraged (28 steps). Proof modification of "reximiaOLD" is discouraged (21 steps). Proof modification of "rexlimivOLD" is discouraged (23 steps). diff --git a/set.mm b/set.mm index 393c847b39..8e53289fd8 100644 --- a/set.mm +++ b/set.mm @@ -30790,6 +30790,69 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is $( *** Theorems using axioms up to ax-9 and ax-ext only: *** $) + ${ + $d x A $. $d x B $. + $( Equality theorem for restricted existential quantifier. (Contributed by + NM, 29-Oct-1995.) Remove usage of ~ ax-10 , ~ ax-11 , and ~ ax-12 . + (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. + (Revised by Wolf Lammen, 8-Mar-2025.) $) + rexeq $p |- ( A = B -> ( E. x e. A ph <-> E. x e. B ph ) ) $= + ( wceq cv wcel wa wex wrex wal dfcleq anbi1 alexbii sylbi df-rex 3bitr4g + wb ) CDEZBFZCGZAHZBIZTDGZAHZBIZABCJABDJSUAUDRZBKUCUFRBCDLUGUBUEBUAUDAMNOA + BCPABDPQ $. + + $( Equality theorem for restricted universal quantifier. (Contributed by + NM, 16-Nov-1995.) Remove usage of ~ ax-10 , ~ ax-11 , and ~ ax-12 . + (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. + (Revised by Wolf Lammen, 8-Mar-2025.) $) + raleq $p |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) ) $= + ( wceq wral wn wrex rexeq exnal 3bitr3g con4bid ) CDEZABCFZABDFZMAGZBCHPB + DHNGOGPBCDIA?JZQKL $. + $} + + ${ + $d A x $. $d B x $. + raleq1i.1 $e |- A = B $. + $( Equality inference for restricted universal quantifier. (Contributed by + Paul Chapman, 22-Jun-2011.) $) + raleqi $p |- ( A. x e. A ph <-> A. x e. B ph ) $= + ( wceq wral wb raleq ax-mp ) CDFABCGABDGHEABCDIJ $. + + $( Equality inference for restricted existential quantifier. (Contributed + by Mario Carneiro, 23-Apr-2015.) $) + rexeqi $p |- ( E. x e. A ph <-> E. x e. B ph ) $= + ( wceq wrex wb rexeq ax-mp ) CDFABCGABDGHEABCDIJ $. + $} + + ${ + $d x A $. $d x B $. + raleqdv.1 $e |- ( ph -> A = B ) $. + $( Equality deduction for restricted universal quantifier. (Contributed by + NM, 13-Nov-2005.) $) + raleqdv $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) ) $= + ( wceq wral wb raleq syl ) ADEGBCDHBCEHIFBCDEJK $. + + $( Equality deduction for restricted existential quantifier. (Contributed + by NM, 14-Jan-2007.) $) + rexeqdv $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) ) $= + ( wceq wrex wb rexeq syl ) ADEGBCDHBCEHIFBCDEJK $. + $} + + ${ + $d x A $. $d x B $. $d x ph $. + raleqbidva.1 $e |- ( ph -> A = B ) $. + raleqbidva.2 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $. + $( Equality deduction for restricted universal quantifier. (Contributed by + Mario Carneiro, 5-Jan-2017.) $) + raleqbidva $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) ) $= + ( wral ralbidva raleqdv bitrd ) ABDEICDEICDFIABCDEHJACDEFGKL $. + + $( Equality deduction for restricted universal quantifier. (Contributed by + Mario Carneiro, 5-Jan-2017.) $) + rexeqbidva $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) ) $= + ( wrex rexbidva rexeqdv bitrd ) ABDEICDEICDFIABCDEHJACDEFGKL $. + $} + ${ $d ph x $. $d A x $. $d B x $. raleqbidvv.1 $e |- ( ph -> A = B ) $. @@ -30797,21 +30860,34 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is $( Version of ~ raleqbidv with additional disjoint variable conditions, not requiring ~ ax-8 nor ~ df-clel . (Contributed by BJ, 22-Sep-2024.) $) raleqbidvv $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) ) $= + ( wb cv wcel adantr raleqbidva ) ABCDEFGABCIDJEKHLM $. + $( $j usage 'raleqbidvv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' + 'df-clel'; $) + + $( Version of ~ raleqbidv with additional disjoint variable conditions, not + requiring ~ ax-8 nor ~ df-clel . (Contributed by BJ, 22-Sep-2024.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + raleqbidvvOLD $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) ) $= ( cv wcel wi wal wral wb wa alrimiv wceq dfcleq sylib df-ral 19.26 imbi12 sylanbrc impcom sylg albi syl 3bitr4g ) ADIZEJZBKZDLZUIFJZCKZDLZBDEMCDFMA UKUNNZDLULUONABCNZUJUMNZOZUPDAUQDLURDLZUSDLAUQDHPAEFQUTGDEFRSUQURDUAUCURU QUPUJUMBCUBUDUEUKUNDUFUGBDETCDFTUH $. - $( $j usage 'raleqbidvv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' - 'df-clel'; $) $( Version of ~ rexeqbidv with additional disjoint variable conditions, not requiring ~ ax-8 nor ~ df-clel . (Contributed by Wolf Lammen, 25-Sep-2024.) $) rexeqbidvv $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) ) $= - ( wrex wn wral notbid raleqbidvv ralnex 3bitr3g con4bid ) ABDEIZCDFIZABJZ - DEKCJZDFKQJRJASTDEFGABCHLMBDENCDFNOP $. + ( wb cv wcel adantr rexeqbidva ) ABCDEFGABCIDJEKHLM $. $( $j usage 'rexeqbidvv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'df-clel'; $) + + $( Version of ~ rexeqbidv with additional disjoint variable conditions, not + requiring ~ ax-8 nor ~ df-clel . (Contributed by Wolf Lammen, + 25-Sep-2024.) (New usage is discouraged.) + (Proof modification is discouraged.) $) + rexeqbidvvOLD $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) ) $= + ( wrex wn wral notbid raleqbidvv ralnex 3bitr3g con4bid ) ABDEIZCDFIZABJZ + DEKCJZDFKQJRJASTDEFGABCHLMBDENCDFNOP $. $} ${ @@ -30834,45 +30910,19 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is $d x A $. $d x B $. $( Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ~ ax-10 , ~ ax-11 , and ~ ax-12 . - (Revised by Steven Nguyen, 30-Apr-2023.) $) - raleq $p |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) ) $= + (Revised by Steven Nguyen, 30-Apr-2023.) (New usage is discouraged.) + (Proof modification is discouraged.) $) + raleqOLD $p |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) ) $= ( wceq biidd raleqbi1dv ) AABCDCDEAFG $. $( Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ~ ax-10 , ~ ax-11 , and ~ ax-12 . - (Revised by Steven Nguyen, 30-Apr-2023.) $) - rexeq $p |- ( A = B -> ( E. x e. A ph <-> E. x e. B ph ) ) $= + (Revised by Steven Nguyen, 30-Apr-2023.) (New usage is discouraged.) + (Proof modification is discouraged.) $) + rexeqOLD $p |- ( A = B -> ( E. x e. A ph <-> E. x e. B ph ) ) $= ( wceq biidd rexeqbi1dv ) AABCDCDEAFG $. $} - ${ - $d A x $. $d B x $. - raleq1i.1 $e |- A = B $. - $( Equality inference for restricted universal quantifier. (Contributed by - Paul Chapman, 22-Jun-2011.) $) - raleqi $p |- ( A. x e. A ph <-> A. x e. B ph ) $= - ( wceq wral wb raleq ax-mp ) CDFABCGABDGHEABCDIJ $. - - $( Equality inference for restricted existential quantifier. (Contributed - by Mario Carneiro, 23-Apr-2015.) $) - rexeqi $p |- ( E. x e. A ph <-> E. x e. B ph ) $= - ( wceq wrex wb rexeq ax-mp ) CDFABCGABDGHEABCDIJ $. - $} - - ${ - $d x A $. $d x B $. - raleqdv.1 $e |- ( ph -> A = B ) $. - $( Equality deduction for restricted universal quantifier. (Contributed by - NM, 13-Nov-2005.) $) - raleqdv $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) ) $= - ( wceq wral wb raleq syl ) ADEGBCDHBCEHIFBCDEJK $. - - $( Equality deduction for restricted existential quantifier. (Contributed - by NM, 14-Jan-2007.) $) - rexeqdv $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) ) $= - ( wceq wrex wb rexeq syl ) ADEGBCDHBCEHIFBCDEJK $. - $} - ${ raleqbii.1 $e |- A = B $. raleqbii.2 $e |- ( ps <-> ch ) $. @@ -30927,21 +30977,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ( cv wcel eleq2d anbi12d rexbidv2 ) ABCDEFADIZEJNFJBCAEFNGKHLM $. $} - ${ - $d x A $. $d x B $. $d x ph $. - raleqbidva.1 $e |- ( ph -> A = B ) $. - raleqbidva.2 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $. - $( Equality deduction for restricted universal quantifier. (Contributed by - Mario Carneiro, 5-Jan-2017.) $) - raleqbidva $p |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) ) $= - ( wral ralbidva raleqdv bitrd ) ABDEICDEICDFIABCDEHJACDEFGKL $. - - $( Equality deduction for restricted universal quantifier. (Contributed by - Mario Carneiro, 5-Jan-2017.) $) - rexeqbidva $p |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) ) $= - ( wrex rexbidva rexeqdv bitrd ) ABDEICDEICDFIABCDEHJACDEFGKL $. - $} - ${ $d A y $. $d ps y $. $d B x $. $d ch x $. $d x ph y $. cbvraldva2.1 $e |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) $. From 5d8df77c90266d5ac7d4e65ddddcf906eb117fae Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sat, 8 Mar 2025 14:53:30 +0100 Subject: [PATCH 7/7] fix proof of raleq --- set.mm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/set.mm b/set.mm index 8e53289fd8..cf9eb8bded 100644 --- a/set.mm +++ b/set.mm @@ -30806,8 +30806,8 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025.) $) raleq $p |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) ) $= - ( wceq wral wn wrex rexeq exnal 3bitr3g con4bid ) CDEZABCFZABDFZMAGZBCHPB - DHNGOGPBCDIA?JZQKL $. + ( wceq wral wn wrex rexeq rexnal 3bitr3g con4bid ) CDEZABCFZABDFZMAGZBCHP + BDHNGOGPBCDIABCJABDJKL $. $} ${