Home | Metamath
Proof ExplorerTheorem List
(p. 291 of 328)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21514) |
Hilbert Space Explorer
(21515-23037) |
Users' Mathboxes
(23038-32776) |

Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|

Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | a9e2ndeqVD 29001* |
The following User's Proof is a Virtual Deduction proof (see: wvd1 28636)
completed automatically by a Metamath tools program invoking mmj2 and
the Metamath Proof Assistant. a9e2eq 28622 is a9e2ndeqVD 29001 without virtual
deductions and was automatically derived from a9e2ndeqVD 29001.
(Contributed by Alan Sare, 25-Mar-2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 2sb5ndVD 29002* |
The following User's Proof is a Virtual Deduction proof (see: wvd1 28636)
completed automatically by a Metamath tools program invoking mmj2 and
the Metamath Proof Assistant. 2sb5nd 28625 is 2sb5ndVD 29002 without virtual
deductions and was automatically derived from 2sb5ndVD 29002. (Contributed
by Alan Sare, 30-Apr-2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 2uasbanhVD 29003* |
The following User's Proof is a Virtual Deduction proof (see: wvd1 28636)
completed automatically by a Metamath tools program invoking mmj2 and
the Metamath Proof Assistant. 2uasbanh 28626 is 2uasbanhVD 29003 without virtual
deductions and was automatically derived from 2uasbanhVD 29003.
(Contributed by Alan Sare, 31-May-2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | e2ebindVD 29004 |
The following User's Proof is a Virtual Deduction proof (see:
wvd1 28636) completed automatically by a Metamath tools program invoking
mmj2 and the Metamath Proof Assistant. e2ebind 28628 is e2ebindVD 29004 without
virtual deductions and was automatically derived from e2ebindVD 29004
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

18.25.8 Virtual Deduction transcriptions of
textbook proofs | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sb5ALTVD 29005* |
The following User's Proof is a Natural Deduction Sequent Calculus
transcription of the Fitch-style Natural Deduction proof of Unit 20
Excercise 3.a., which is sb5 2052, found in the "Answers to Starred
Exercises" on page 457 of "Understanding Symbolic Logic", Fifth
Edition (2008), by Virginia Klenk. The same proof may also be
interpreted as a Virtual Deduction Hilbert-style axiomatic proof. It
was completed automatically by the tools program completeusersproof.cmd,
which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof
Assistant. sb5ALT 28587 is sb5ALTVD 29005 without virtual deductions and
was automatically derived from sb5ALTVD 29005.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | vk15.4jVD 29006 |
The following User's Proof is a Natural Deduction Sequent Calculus
transcription of the Fitch-style Natural Deduction proof of Unit 15
Excercise 4.f. found in the "Answers to Starred Exercises" on page 442
of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia
Klenk. The same proof may also be interpreted to be a Virtual Deduction
Hilbert-style axiomatic proof. It was completed automatically by the
tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and
Norm Megill's Metamath Proof Assistant. vk15.4j 28590 is vk15.4jVD 29006
without virtual deductions and was automatically derived
from vk15.4jVD 29006. Step numbers greater than 25 are additional steps
necessary for the sequent calculus proof not contained in the
Fitch-style proof. Otherwise, step i of the User's Proof corresponds to
step i of the Fitch-style proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | notnot2ALTVD 29007 |
The following User's Proof is a Natural Deduction Sequent Calculus
transcription of the Fitch-style Natural Deduction proof of Theorem 5 of
Section 14 of [Margaris] p. 59 ( which is notnot2 104). The same proof
may also be interpreted as a Virtual Deduction Hilbert-style
axiomatic proof. It was completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's
Metamath Proof Assistant. notnot2ALT 28591 is notnot2ALTVD 29007
without virtual deductions and was automatically derived
from notnot2ALTVD 29007. Step i of the User's Proof corresponds to
step i of the Fitch-style proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | con3ALTVD 29008 |
The following User's Proof is a Natural Deduction Sequent Calculus
transcription of the Fitch-style Natural Deduction proof of Theorem 7 of
Section 14 of [Margaris] p. 60 ( which is con3 126). The same proof
may also be interpreted to be a Virtual Deduction Hilbert-style
axiomatic proof. It was completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's
Metamath Proof Assistant. con3ALT 28592 is con3ALTVD 29008
without virtual deductions and was automatically derived
from con3ALTVD 29008. Step i of the User's Proof corresponds to
step i of the Fitch-style proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

18.25.9 Theorems proved using conjunction-form
virtual deduction | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | elpwgdedVD 29009 | Membership in a power class. Theorem 86 of [Suppes] p. 47. Derived from elpwg 3645. In form of VD deduction with and as variable virtual hypothesis collections based on Mario Carneiro's metavariable concept. elpwgded 28629 is elpwgdedVD 29009 using conventional notation. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sspwimp 29010 | If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. sspwimp 29010, using conventional notation, was translated from virtual deduction form, sspwimpVD 29011, using a translation program. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sspwimpVD 29011 |
The following User's Proof is a Virtual Deduction proof ( see: wvd1 28636)
using conjunction-form virtual hypothesis collections. It was completed
manually, but has the potential to be completed automatically by a tools
program which would invoke Mel O'Cat's mmj2 and Norm Megill's Metamath
Proof Assistant. sspwimp 29010 is sspwimpVD 29011 without virtual deductions and
was derived from sspwimpVD 29011. (Contributed by Alan Sare, 23-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sspwimpcf 29012 | If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. sspwimpcf 29012, using conventional notation, was translated from its virtual deduction form, sspwimpcfVD 29013, using a translation program. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sspwimpcfVD 29013 |
The following User's Proof is a Virtual Deduction proof ( see: wvd1 28636)
using conjunction-form virtual hypothesis collections. It was completed
automatically by a tools program which would invokes Mel O'Cat's mmj2
and Norm Megill's Metamath Proof Assistant. sspwimpcf 29012 is sspwimpcfVD 29013
without virtual deductions and was derived from sspwimpcfVD 29013. The
version of completeusersproof.cmd used is capable of only generating
conjunction-form unification theorems, not unification deductions.
(Contributed by Alan Sare, 13-Jun-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | suctrALTcf 29014 | The sucessor of a transitive class is transitive. suctrALTcf 29014, using conventional notation, was translated from virtual deduction form, suctrALTcfVD 29015, using a translation program. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | suctrALTcfVD 29015 |
The following User's Proof is a Virtual Deduction proof ( see: wvd1 28636)
using conjunction-form virtual hypothesis collections. The
conjunction-form version of completeusersproof.cmd. It allows the User
to avoid superflous virtual hypotheses. This proof was completed
automatically by a tools program which invokes Mel O'Cat's
mmj2 and Norm Megill's Metamath Proof Assistant. suctrALTcf 29014
is suctrALTcfVD 29015 without virtual deductions and was derived
automatically from suctrALTcfVD 29015. The version of
completeusersproof.cmd used is capable of only generating
conjunction-form unification theorems, not unification deductions.
(Contributed by Alan Sare, 13-Jun-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

18.25.10 Theorems with VD proofs in
conventional notation derived from VD proofs | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | suctrALT3 29016 | The successor of a transtive class is transitive. suctrALT3 29016 is the completed proof in conventional notation of the Virtual Deduction proof http://www.virtualdeduction.com/suctralt3vd.html. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 28636 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction ( e.g. , the sub-theorem whose assertion is step 19 used jaoded 28631). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem ( e.g. , the sub-theorem whose assertion is step 24 used dftr2 4131) . (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sspwimpALT 29017 | If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. sspwimpALT 29017 is the completed proof in conventional notation of the Virtual Deduction proof http://www.virtualdeduction.com/sspwimpaltvd.html. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 28636 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction ( e.g. , the sub-theorem whose assertion is step 9 used elpwgded 28629). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem ( e.g. , the sub-theorem whose assertion is step 5 used elpwi 3646) . (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | unisnALT 29018 | A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. The User manually input on a mmj2 Proof Worksheet, without labels, all steps of unisnALT 29018 except 1, 11, 15, 21, and 30. With execution of the mmj2 unification command, mmj2 could find labels for all steps except for 2, 12, 16, 22, and 31 (and the then non-existing steps 1, 11, 15, 21, and 30) . mmj2 could not find reference theorems for those five steps because the hypothesis field of each of these steps was empty and none of those steps unifies with a theorem in set.mm. Each of these five steps is a semantic variation of a theorem in set.mm and is 2-step provable. mmj2 does not have the ability to automatically generate the semantic variation in set.mm of a theorem in a mmj2 Proof Worksheet unless the theorem in the Proof Worksheet is labeled with a 1-hypothesis deduction whose hypothesis is a theorem in set.mm which unifies with the theorem in the Proof Worksheet. The stepprover.c program, which invokes mmj2, has this capability. stepprover.c automatically generated steps 1, 11, 15, 21, and 30, labeled all steps, and generated the RPN proof of unisnALT 29018. Roughly speaking, stepprover.c added to the Proof Worksheet a labeled duplicate step of each non-unifying theorem for each label in a text file, labels.txt, containing a list of labels provided by the User. Upon mmj2 unification, stepprover.c identified a label for each of the five theorems which 2-step proves it. For unisnALT 29018, the label list is a list of all 1-hypothesis propositional calculus deductions in set.mm. stepproverp.c is the same as stepprover.c except that it intermittently pauses during execution, allowing the User to observe the changes to a text file caused by the execution of particular statements of the program. (Contributed by Alan Sare, 19-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

18.25.11 Theorems with a proof in conventional
notation automatically derivedby completeusersproof.c from a Virtual Deduction User's Proof | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | notnot2ALT2 29019 | Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. (Contributed by Alan Sare, 11-Sep-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | suctrALT4 29020 | The sucessor of a transitive class is transitive. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in http://www.virtualdeduction.com/suctralt3vd.html. (Contributed by Alan Sare, 11-Sep-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sspwimpALT2 29021 | If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in http://www.virtualdeduction.com/sspwimpaltvd.html. (Contributed by Alan Sare, 11-Sep-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | e2ebindALT 29022 | Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in e2ebindVD 29004. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | a9e2ndALT 29023* | If at least two sets exist (dtru 4217) , then the same is true expressed in an alternate form similar to the form of a9e 1904. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in a9e2ndVD 29000. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | a9e2ndeqALT 29024* | "At least two sets exist" expressed in the form of dtru 4217 is logically equivalent to the same expressed in a form similar to a9e 1904 if dtru 4217 is false implies . Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in a9e2ndeqVD 29001. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 2sb5ndALT 29025* | Equivalence for double substitution 2sb5 2064 without distinct , requirement. 2sb5nd 28625 is derived from 2sb5ndVD 29002. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in 2sb5ndVD 29002. (Contributed by Alan Sare, 19-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | chordthmALT 29026* |
The intersecting chords theorem. If points A, B, C, and D lie on a
circle (with center Q, say), and the point P is on the interior of the
segments AB and CD, then the two products of lengths PA PB and
PC PD are equal. The Euclidean plane is identified with the
complex plane, and the fact that P is on AB and on CD is expressed by
the hypothesis that the angles APB and CPD are equal to . The
result is proven by using chordthmlem5 20149 twice to show that PA
PB and PC PD both equal BQ
^{2}
PQ
^{2}
. This is similar to the proof of the
theorem given in Euclid's Elements_, where it is Proposition III.35.
Proven by David Moews on 28-Feb-2017 as chordthm 20150.
http://www.virtualdeduction.com/chordthmaltvd.html
is a Virtual
Deduction User's Proof transcription of chordthm 20150. That VD User's
Proof was input into completeusersproof, automatically generating this
chordthmALT 29026 Metamath proof. (Contributed by Alan Sare,
19-Sep-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

18.26 Mathbox for Jonathan
Ben-NaimNote: On 4-Sep-2016 and after, 745 unused theorems were deleted from this mathbox, and 359 theorems used only once or twice were merged into their referencing theorems. The originals can be recovered from set.mm versions prior to this date. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | w-bnj17 29027 | Extend wff notation with the 4-way conjunction. (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-bnj17 29028 | Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | c-bnj14 29029 | Extend class notation with the function giving: the class of all elements of that are "smaller" than according to . (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-bnj14 29030* | Define the function giving: the class of all elements of that are "smaller" than according to . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | w-bnj13 29031 | Extend wff notation with the following predicate: is set-like on . (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-bnj13 29032* | Define the following predicate: is set-like on . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | w-bnj15 29033 | Extend wff notation with the following predicate: is both well-founded and set-like on . (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-bnj15 29034 | Define the following predicate: is both well-founded and set-like on . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | c-bnj18 29035 | Extend class notation with the function giving: the transitive closure of in by . (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-bnj18 29036* | Define the function giving: the transitive closure of in by . This definition has been designed for facilitating verification that it is eliminable and that the $d restrictions are sound and complete. For a more readable definition see bnj882 29274. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | w-bnj19 29037 | Extend wff notation with the following predicate: is transitive for and . (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-bnj19 29038* | Define the following predicate: is transitive for and . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

18.26.1 First order logic and set
theory | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj170 29039 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj240 29040 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj248 29041 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj250 29042 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj251 29043 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj252 29044 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj253 29045 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj255 29046 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj256 29047 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj257 29048 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj258 29049 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj268 29050 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj290 29051 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj291 29052 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj312 29053 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj334 29054 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj345 29055 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj422 29056 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj432 29057 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj446 29058 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj21 29059* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj23 29060* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj31 29061 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj62 29062* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj89 29063* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj90 29064* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj101 29065 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj105 29066 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj115 29067 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj132 29068* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj133 29069 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj142 29070 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj145 29071 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj156 29072 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj158 29073* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj168 29074* | First-order logic and set theory. Revised to remove dependence on ax-reg 7322. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by NM, 21-Dec-2016.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj206 29075 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj216 29076 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj219 29077 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj226 29078* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj228 29079 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj519 29080 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj521 29081 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj524 29082 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj525 29083* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj534 29084* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj538 29085* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj529 29086 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj551 29087 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj563 29088 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj564 29089 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj593 29090 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj596 29091 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj610 29092* | Pass from equality ( ) to substitution ( ) without the distinct variable restriction ($d ). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj642 29093 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj643 29094 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj645 29095 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj658 29096 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj667 29097 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj705 29098 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj706 29099 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj707 29100 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |