From 194b0585615b503c62a58b42b9e3fd30a60ad87e Mon Sep 17 00:00:00 2001 From: glacode Date: Sat, 25 Jan 2025 17:00:24 +0100 Subject: [PATCH] Move ~ rextru to Main (#4599) --- changes-set.txt | 1 + set.mm | 12 ++++++------ 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/changes-set.txt b/changes-set.txt index d31c8cf2a7..09dee27821 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -87,6 +87,7 @@ make a github issue.) DONE: Date Old New Notes +24-Jan-25 rextru [same] Moved from ZW's mathbox to main set.mm 19-Jan-25 --- --- Moved surreal cut and option theorems from SF's mathbox to main set.mm 19-Jan-25 imaindm [same] Moved from SF's mathbox to main set.mm diff --git a/set.mm b/set.mm index 27178745f2..4d36fd2e2d 100644 --- a/set.mm +++ b/set.mm @@ -28455,6 +28455,12 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is rexex $p |- ( E. x e. A ph -> E. x ph ) $= ( wrex cv wcel wa wex df-rex exsimpr sylbi ) ABCDBECFZAGBHABHABCILABJK $. + $( Two ways of expressing that a class has at least one element. + (Contributed by Zhi Wang, 23-Sep-2024.) $) + rextru $p |- ( E. x x e. A <-> E. x e. A T. ) $= + ( cv wcel wex wtru wa wrex tru biantru exbii df-rex bitr4i ) ACBDZAENFGZAEF + ABHNOAFNIJKFABLM $. + ${ ralimi2.1 $e |- ( ( x e. A -> ph ) -> ( x e. B -> ps ) ) $. $( Inference quantifying both antecedent and consequent. (Contributed by @@ -789991,12 +789997,6 @@ additional condition (deduction form). See ~ ralbidc for a more GODTIJBDEFGKPQRS $. $} - $( Two ways of expressing "at least one" element. (Contributed by Zhi Wang, - 23-Sep-2024.) $) - rextru $p |- ( E. x x e. A <-> E. x e. A T. ) $= - ( cv wcel wex wtru wa wrex tru biantru exbii df-rex bitr4i ) ACBDZAENFGZAEF - ABHNOAFNIJKFABLM $. - $( Two ways of expressing "at most one" element. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof shortened by BJ, 23-Sep-2024.) $) rmotru $p |- ( E* x x e. A <-> E* x e. A T. ) $=