Home | Metamath
Proof ExplorerTheorem List
(p. 278 of 313)
| < 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-21423) |
Hilbert Space Explorer
(21424-22946) |
Users' Mathboxes
(22947-31284) |

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

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

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

16.22.6 Virtual Deduction transcriptions of
textbook proofs | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sb5ALTVD 27702* |
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 1994, 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 27304 is sb5ALTVD 27702 without virtual deductions and
was automatically derived from sb5ALTVD 27702.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | vk15.4jVD 27703 |
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 27307 is vk15.4jVD 27703
without virtual deductions and was automatically derived
from vk15.4jVD 27703. 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 27704 |
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 106). 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 27308 is notnot2ALTVD 27704
without virtual deductions and was automatically derived
from notnot2ALTVD 27704. Step i of the User's Proof corresponds to
step i of the Fitch-style proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | con3ALTVD 27705 |
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 128). 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 27309 is con3ALTVD 27705
without virtual deductions and was automatically derived
from con3ALTVD 27705. Step i of the User's Proof corresponds to
step i of the Fitch-style proof.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

Theorem | sspwimp 27707 | 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 27707, using conventional notation, was translated from virtual deduction form, sspwimpVD 27708, using a translation program. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

Theorem | sspwimpcf 27709 | 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 27709, using conventional notation, was translated from its virtual deduction form, sspwimpcfVD 27710, using a translation program. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sspwimpcfVD 27710 |
The following User's Proof is a Virtual Deduction proof ( see: wvd1 27353)
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 27709 is sspwimpcfVD 27710
without virtual deductions and was derived from sspwimpcfVD 27710. 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 27711 | The sucessor of a transitive class is transitive. suctrALTcf 27711, using conventional notation, was translated from virtual deduction form, suctrALTcfVD 27712, using a translation program. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | suctrALTcfVD 27712 |
The following User's Proof is a Virtual Deduction proof ( see: wvd1 27353)
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 27711
is suctrALTcfVD 27712 without virtual deductions and was derived
automatically from suctrALTcfVD 27712. 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.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

Theorem | suctrALT3 27713 | The successor of a transtive class is transitive. suctrALT3 27713 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 27353 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 27348). 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 4055) . (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sspwimpALT 27714 | 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 27714 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 27353 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 27346). 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 3574) . (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | unisnALT 27715 | 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 27715 except 1, 11, 15, 21, and 30. With execution of the mmj2 unification command, mmj2 could find labels for all of 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 an 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 27715. 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 27715, 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

Theorem | notnot2ALT2 27716 | 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 27717 | 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 27718 | 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 27719 | 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 27701. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | a9e2ndALT 27720* | If at least two sets exist (dtru 4139) , then the same is true expressed in an alternate form similar to the form of a9e 1817. 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 27697. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | a9e2ndeqALT 27721* | "At least two sets exist" expressed in the form of dtru 4139 is logically equivalent to the same expressed in a form similar to a9e 1817 if dtru 4139 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 27698. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 2sb5ndALT 27722* | Equivalence for double substitution 2sb5 2075 without distinct , requirement. 2sb5nd 27342 is derived from 2sb5ndVD 27699. 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 27699. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

16.23 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 27723 | Extend wff notation with the 4-way conjunction. (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

Syntax | c-bnj14 27725 | 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 27726* | 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 27727 | Extend wff notation with the following predicate: is set-like on . (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

Definition | df-bnj15 27730 | 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 27731 | Extend class notation with the function giving: the transitive closure of in by . (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-bnj18 27732* | 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 27970. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

16.23.1 First order logic and set
theory | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem | bnj422 27752 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

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

Theorem | bnj23 27756* | 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 27757 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

Theorem | bnj89 27759* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj90 27760* | 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 27761 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj105 27762 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj115 27763 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj132 27764* | 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 27765 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj142 27766 | 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 27767 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj156 27768 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj158 27769* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

Theorem | bnj206 27771 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj216 27772 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj219 27773 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj226 27774* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj228 27775 | 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 27776 | 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 27777 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj524 27778 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj525 27779* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj534 27780* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj538 27781* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj529 27782 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj551 27783 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj563 27784 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj564 27785 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj593 27786 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj596 27787 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | bnj610 27788* | 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 27789 | -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

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

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

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

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

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

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

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

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

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

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |