HomeTheorem List (p. 292 of 325)
Unicode version.
| Home |
Metamath
Proof Explorer Theorem List (p. 292 of 325) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-22374) |
Hilbert Space Explorer
(22375-23897) |
Users' Mathboxes
(23898-32447) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | bnj1326 29101* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
       
 ![/\](wedge.gif "/\"){kind=small}       
        
         
 | ||
| Theorem | bnj1321 29102* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
     | ||
| Theorem | bnj1364 29103 |
Property of .
(Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(New usage is discouraged.)
|
 | ||
| Theorem | bnj1371 29104* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
         ![].](_drbrack.gif "]."){kind=small} 
   | ||
| Theorem | bnj1373 29105* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1374 29106* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1384 29107* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1388 29108* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1398 29109* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
   
| ||
| Theorem | bnj1413 29110* |
Property of .
(Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.)
|
 | ||
| Theorem | bnj1408 29111* | Technical lemma for bnj1414 29112. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1414 29112* |
Property of .
(Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.)
|
|
| ||
| Theorem | bnj1415 29113* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1416 29114 | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1418 29115 |
Property of .
(Contributed by Jonathan Ben-Naim,
3-Jun-2011.) (New usage is discouraged.)
|
|
| ||
| Theorem | bnj1417 29116* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
| ||
| Theorem | bnj1421 29117* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1444 29118* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 
| ||
| Theorem | bnj1445 29119* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1446 29120* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1447 29121* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1448 29122* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1449 29123* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1442 29124* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1450 29125* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1423 29126* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1452 29127* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1466 29128* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 | ||
| Theorem | bnj1467 29129* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1463 29130* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1489 29131* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1491 29132* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1312 29133* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1493 29134* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1497 29135* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1498 29136* | Technical lemma for bnj60 29137. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 | ||
| Theorem | bnj60 29137* | Well-founded recursion, part 1 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1514 29138* | Technical lemma for bnj1500 29143. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1518 29139* | Technical lemma for bnj1500 29143. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1519 29140* | Technical lemma for bnj1500 29143. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1520 29141* | Technical lemma for bnj1500 29143. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1501 29142* | Technical lemma for bnj1500 29143. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1500 29143* | Well-founded recursion, part 2 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1525 29144* | Technical lemma for bnj1522 29147. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1529 29145* | Technical lemma for bnj1522 29147. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1523 29146* | Technical lemma for bnj1522 29147. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1522 29147* | Well-founded recursion, part 3 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
Note: A label suffixed with "N" (after the "Atoms..." section below), such as lshpnel2N 29468, means that the definition or theorem is not used for the derivation of hlathil 32447. This is a temporary renaming to assist cleaning up the theorems needed by hlathil 32447. Please inform me of any changes that might affect my mathbox, since I may be working on it independently of the github commits. - Norm 30-Nov-2015 | ||
This section reproduces all predicate calculus theorems through sbal2 2184 that depend on ax-7 1745. It is an experiment to see how much of predicate calculus can be derived using the weaker (unbundled) ax-7v 29148. The theorems in this section with suffix "NEW7" are direct replacements for the existing ones without the suffix but have proofs that avoid ax-7 1745 in favor of ax-7v 29148. Theorems with suffix "AUX7" are new theorems that do not appear in the main predicate calculus section but assist the proofs of the "NEW7" suffixed theorems. They also use at most ax-7v 29148 and not ax-7 1745. Theorems with suffix "OLD7" are the remaining predicate calculus theorems (through sbal2 2184) that haven't been proved from ax-7v 29148. In order to isolate them, they are derived from ax-7OLD7 29362 which replicates ax-7 1745. Whenever a proof of a *OLD7 theorem is found from ax-7v 29148, the suffix is changed to "NEW7" and the theorem is moved up to the "NEW7" section. Theorems with suffix "AUXOLD7" (currently just nfsb4tw2AUXOLD7 29430) are results of an unsuccessful attempt to prove a helper theorem from ax-7v 29148, but still needs the help of ax-7 1745. Currently there are about 137 "NEW7" theorems (starting after ax-7v 29148) and 91 "OLD7" theorems (starting after ax-7OLD7 29362). | ||
| Axiom | ax-7v 29148* | Experiment to see if ax-7 1745 can be unbundled i.e. can be derived from ax-7v 29148. This axiom is temporary. It will be replaced with a theorem derived from ax-7 1745 if we are successful, otherwise will be deleted. (Contributed by NM, 9-Oct-2017.) |
| | ||
| Theorem | ax7vAUX7 29149* |
A weaker version of ax-7 1745 with distinct variable restrictions. In
order to show that this weakening is adequate, this should be the only
theorem referencing ax-7 1745 directly.
(Right now we derive this from the temporary axiom ax-7v 29148 for easier 'show trace'. If this project is successful, which is seeming more and more unlikely, we will derive this from ax-7 1745 just as we derive ax9v 1663 from ax-9 1662.) (Contributed by NM, 9-Oct-2017.) |
| | ||
| Theorem | alcomwAUX7 29150* | Weak version of alcom 1748 not requiring ax-7 1745. (Contributed by NM, 27-Oct-2017.) |
| | ||
| Theorem | a7swAUX7 29151* | Weak version of a7s 1746 not requiring ax-7 1745. (Contributed by NM, 28-Oct-2017.) |
|
| ||
| Theorem | cbv3hvNEW7 29152* | Lemma for ax10NEW7 29179. Similar to cbv3h 2036. Requires distinct variables but avoids ax-12 1946. (Contributed by NM, 25-Jul-2015.) (Revised by NM, 25-Nov-2017.) Revised to prove from ax-7v 29148 instead of ax-7 1745. |
|
| ||
| Theorem | hbalw2AUX7 29153* | Weak version of hbal 1747 not requiring ax-7 1745. (Contributed by NM, 9-Oct-2017.) |
| | ||
| Theorem | hbaldwAUX7 29154* | Weak version of hbald 1751 not requiring ax-7 1745. (Contributed by NM, 9-Oct-2017.) |
|
| ||
| Theorem | hbexwAUX7 29155* | Weak version of hbex 1859 not requiring ax-7 1745. (Contributed by NM, 9-Oct-2017.) |
| | ||
| Theorem | nfalwAUX7 29156* | Weak version of nfal 1860 not requiring ax-7 1745. (Contributed by NM, 27-Oct-2017.) |
 | ||
| Theorem | nfexwAUX7 29157* | Weak version of nfex 1861 not requiring ax-7 1745. (Contributed by NM, 27-Oct-2017.) |
| | ||
| Theorem | nfaldwAUX7 29158* | Weak version of nfald 1867 not requiring ax-7 1745. (Contributed by NM, 27-Oct-2017.) |
| | ||
| Theorem | nfexdwAUX7 29159* | Weak version of nfexd 1869 not requiring ax-7 1745. (Contributed by NM, 27-Oct-2017.) |
| | ||
| Theorem | 19.12vAUX7 29160* | Weak version of 19.12 1865 not requiring ax-7 1745. (Contributed by NM, 10-Oct-2017.) |
| | ||
| Theorem | dvelimhwNEW7 29161* | Proof of dvelimh 2015 without using ax-12 1946 but with additional distinct variable conditions. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) |
|
| ||
| Theorem | ax12olem2wAUX7 29162* | Lemma for ax12o 1976. Negate the equalities in ax-12 1946, shown as the hypothesis. (Contributed by NM, 10-Oct-2017.) |
|
| ||
| Theorem | ax12olem3aAUX7 29163 | Lemma for ax12o 1976. Show the equivalence of an intermediate equivalent to ax12o 1976 with the conjunction of ax-12 1946 and a variant with negated equalities. (Contributed by NM, 29-Oct-2017.) |
|
| ||
| Theorem | ax12olem4wAUX7 29164* | Lemma for ax12o 1976. Construct an intermediate equivalent to ax-12 1946 from two instances of ax-12 1946. (Contributed by NM, 10-Oct-2017.) |
|
| ||
| Theorem | ax12olem6NEW7 29165* | Lemma for ax12o 1976. Derivation of ax12o 1976 from the hypotheses, without using ax12o 1976. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 24-Dec-2015.) |
|
| ||
| Theorem | ax12olem7NEW7 29166* | Lemma for ax12o 1976. Derivation of ax12o 1976 from the hypotheses, without using ax12o 1976. (Contributed by NM, 24-Dec-2015.) |
|
| ||
| Theorem | ax12oNEW7 29167 | Derive set.mm's original ax-12o 2192 from the shorter ax-12 1946. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) |
|
| ||
| Theorem | dvelimvNEW7 29168* | Similar to dvelim 2066 with first hypothesis replaced by distinct variable condition. (Contributed by NM, 25-Jul-2015.) |
|
| ||
| Theorem | dveeq2NEW7 29169* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) |
|
| ||
| Theorem | dveeq1NEW7 29170* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
|
| ||
| Theorem | dveel1NEW7 29171* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
|
| ||
| Theorem | dveel2NEW7 29172* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
|
| ||
| Theorem | dvelimwAUX7 29173* | Weaker version of dvelim 2066. (Contributed by NM, 23-Nov-1994.) |
|
| ||
| Theorem | ax9NEW7 29174 |
Theorem showing that ax-9 1662 follows from the weaker version ax9v 1663.
(Even though this theorem depends on ax-9 1662,
all references of ax-9 1662
are made via ax9v 1663. An earlier version stated ax9v 1663
as a separate
axiom, but having two axioms caused some confusion.)
This theorem should be referenced in place of ax-9 1662 so that all proofs can be traced back to ax9v 1663. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) |
| | ||
| Theorem | ax9oNEW7 29175 |
Show that the original axiom ax-9o 2188 can be derived from ax9 1949
and
others. See ax9from9o 2198 for the rederivation of ax9 1949
from ax-9o 2188.
Normally, ax9o 1950 should be used rather than ax-9o 2188, except by theorems specifically studying the latter's properties. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) |
|
| ||
| Theorem | a9eNEW7 29176 | At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 1563 through ax-14 1725 and ax-17 1623, all axioms other than ax9 1949 are believed to be theorems of free logic, although the system without ax9 1949 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) |
|
| ||
| Theorem | ax10lem4NEW7 29177* | Lemma for ax10 1991. Change bound variable. (Contributed by NM, 8-Jul-2016.) |
|
| ||
| Theorem | ax10lem5NEW7 29178* | Lemma for ax10 1991. Change free and bound variables. (Contributed by NM, 22-Jul-2015.) |
|
| ||
| Theorem | ax10NEW7 29179 | Derive set.mm's original ax-10 2190 from others. (Contributed by NM, 25-Jul-2015.) (Revised by NM, 7-Nov-2015.) |
|
| ||
| Theorem | aecomNEW7 29180 |
Commutation law for identical variable specifiers. The antecedent and
consequent are true when and are
substituted with the same
variable. Lemma L12 in [Megill] p. 445
(p. 12 of the preprint).
(Contributed by NM, 5-Aug-1993.)
|
|
| ||
| Theorem | aecomsNEW7 29181 | A commutation rule for identical variable specifiers. (Contributed by NM, 5-Aug-1993.) |
|
| ||
| Theorem | ax10oNEW7 29182 | Show that ax-10o 2189 can be derived from ax-10 2190 in the form of ax10 1991. Normally, ax10o 2001 should be used rather than ax-10o 2189, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) |
|
| ||
| Theorem | hba1eAUX7 29183 | Special case of hbae 2005 not requiring ax-7 1745. (Contributed by NM, 12-Oct-2017.) |
|
| ||
| Theorem | hbaewAUX7 29184* | Weak version of hbae 2005 not requiring ax-7 1745. See hbaew2AUX7 29185 and hbaew3AUX7 29228 for versions with different distinct variable requirements. (Contributed by NM, 10-Oct-2017.) |
|
| ||
| Theorem | hbaew2AUX7 29185* | Weak version of hbae 2005 not requiring ax-7 1745. Different distinct variable requirements from hbaewAUX7 29184. (Contributed by NM, 30-Oct-2017.) |
|
| ||
| Theorem | nfaewAUX7 29186* | Weak version of nfae 2006 not requiring ax-7 1745. (Contributed by NM, 10-Oct-2017.) |
| | ||
| Theorem | hbnaewAUX7 29187* | Weak version of hbnae 2007 not requiring ax-7 1745. (Contributed by NM, 10-Oct-2017.) |
|
| ||
| Theorem | nfnaewAUX7 29188* | Weak version of nfnae 2008 not requiring ax-7 1745. (Contributed by NM, 27-Oct-2017.) |
| | ||
| Theorem | nfaew2AUX7 29189* | Weak version of nfae 2006 not requiring ax-7 1745. (Contributed by NM, 25-Nov-2017.) |
| | ||
| Theorem | hbnaew2AUX7 29190* | Weak version of hbnae 2007 not requiring ax-7 1745. (Contributed by NM, 25-Nov-2017.) |
|
| ||
| Theorem | nfnaew2AUX7 29191* | Weak version of nfnae 2008 not requiring ax-7 1745. (Contributed by NM, 25-Nov-2017.) |
| | ||
| Theorem | nfeqfNEW7 29192 |
A variable is effectively not free in an equality if it is not either of
the involved variables. version of ax-12o 2192. (Contributed by
Mario Carneiro, 6-Oct-2016.)
|
|
| ||
| Theorem | equsalNEW7 29193 | A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) |
|
| ||
| Theorem | equsalihAUX7 29194 | One direction of equsalhNEW7 29195 with weaker hypothesis. TO DO: Delete if not used. (Contributed by NM, 13-Nov-2017.) |
|
| ||
| Theorem | equsalhNEW7 29195 | A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.) |
|
| ||
| Theorem | equsexNEW7 29196 | A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
|
| ||
| Theorem | equsexhNEW7 29197 | A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.) |
|
| ||
| Theorem | dvelimhvAUX7 29198* | Weak version of dvelimh 2015 not requiring ax-7 1745. (Contributed by NM, 10-Oct-2017.) |
|
| ||
| Theorem | dral1NEW7 29199 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 24-Nov-1994.) |
|
| ||
| Theorem | drex1NEW7 29200 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |