Home | Metamath
Proof Explorer Theorem List (p. 28 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3eltr4i 2701 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐶 ∈ 𝐷 | ||
Theorem | 3eltr3d 2702 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | 3eltr4d 2703 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | 3eltr3g 2704 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | 3eltr4g 2705 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | eleq2s 2706 | Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝐴 ∈ 𝐵 → 𝜑) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝐴 ∈ 𝐶 → 𝜑) | ||
Theorem | eqneltrd 2707 | If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | eqneltrrd 2708 | If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.) (Proof shortened by Wolf Lammen, 13-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶) | ||
Theorem | neleqtrd 2709 | If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) | ||
Theorem | neleqtrrd 2710 | If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.) (Proof shortened by Wolf Lammen, 13-Nov-2019.) |
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) | ||
Theorem | cleqh 2711* | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2776. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2019.) Remove dependency on ax-13 2234. (Revised by BJ, 30-Nov-2020.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) & ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | nelneq 2712 | A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.) |
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵) | ||
Theorem | nelneq2 2713 | A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶) | ||
Theorem | eqsb3lem 2714* | Lemma for eqsb3 2715. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ ([𝑥 / 𝑦]𝑦 = 𝐴 ↔ 𝑥 = 𝐴) | ||
Theorem | eqsb3 2715* | Substitution applied to an atomic wff (class version of equsb3 2420). (Contributed by Rodolfo Medina, 28-Apr-2010.) |
⊢ ([𝑥 / 𝑦]𝑦 = 𝐴 ↔ 𝑥 = 𝐴) | ||
Theorem | clelsb3 2716* | Substitution applied to an atomic wff (class version of elsb3 2422). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ ([𝑥 / 𝑦]𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴) | ||
Theorem | hbxfreq 2717 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1742 for equivalence version. (Contributed by NM, 21-Aug-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | ||
Theorem | hblem 2718* | Change the free variable of a hypothesis builder. Lemma for nfcrii 2744. (Contributed by NM, 21-Jun-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴) | ||
Theorem | abeq2 2719* |
Equality of a class variable and a class abstraction (also called a
class builder). Theorem 5.1 of [Quine]
p. 34. This theorem shows the
relationship between expressions with class abstractions and expressions
with class variables. Note that abbi 2724 and its relatives are among
those useful for converting theorems with class variables to equivalent
theorems with wff variables, by first substituting a class abstraction
for each class variable.
Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable 𝜑 (that has a free variable 𝑥) to a theorem with a class variable 𝐴, we substitute 𝑥 ∈ 𝐴 for 𝜑 throughout and simplify, where 𝐴 is a new class variable not already in the wff. An example is the conversion of zfauscl 4711 to inex1 4727 (look at the instance of zfauscl 4711 that occurs in the proof of inex1 4727). Conversely, to convert a theorem with a class variable 𝐴 to one with 𝜑, we substitute {𝑥 ∣ 𝜑} for 𝐴 throughout and simplify, where 𝑥 and 𝜑 are new setvar and wff variables not already in the wff. Examples include dfsymdif2 3813 and cp 8637; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 8636. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 26-May-1993.) |
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | abeq1 2720* | Equality of a class variable and a class abstraction. Commuted form of abeq2 2719. (Contributed by NM, 20-Aug-1993.) |
⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝑥 ∈ 𝐴)) | ||
Theorem | abeq2d 2721 | Equality of a class variable and a class abstraction (deduction form of abeq2 2719). (Contributed by NM, 16-Nov-1995.) |
⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) | ||
Theorem | abeq2i 2722 | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 3-Apr-1996.) (Proof shortened by Wolf Lammen, 15-Nov-2019.) |
⊢ 𝐴 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) | ||
Theorem | abeq1i 2723 | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 31-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Nov-2019.) |
⊢ {𝑥 ∣ 𝜑} = 𝐴 ⇒ ⊢ (𝜑 ↔ 𝑥 ∈ 𝐴) | ||
Theorem | abbi 2724 | Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) | ||
Theorem | abbi2i 2725* | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 26-May-1993.) |
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) ⇒ ⊢ 𝐴 = {𝑥 ∣ 𝜑} | ||
Theorem | abbii 2726 | Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} | ||
Theorem | abbid 2727 | Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) | ||
Theorem | abbidv 2728* | Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) | ||
Theorem | abbi2dv 2729* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) | ||
Theorem | abbi1dv 2730* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴) | ||
Theorem | abid1 2731* |
Every class is equal to a class abstraction (the class of sets belonging
to it). Theorem 5.2 of [Quine] p. 35.
This is a generalization to
classes of cvjust 2605. The proof does not rely on cvjust 2605, so cvjust 2605
could be proved as a special instance of it. Note however that abid1 2731
necessarily relies on df-clel 2606, whereas cvjust 2605 does not.
This theorem requires ax-ext 2590, df-clab 2597, df-cleq 2603, df-clel 2606, but to prove that any specific class term not containing class variables is a setvar or can be written as (is equal to) a class abstraction does not require these $a-statements. This last fact is a metatheorem, consequence of the fact that the only $a-statements with typecode class are cv 1474, cab 2596 and statements corresponding to defined class constructors. Note on the simultaneous presence in set.mm of this abid1 2731 and its commuted form abid2 2732: It is rare that two forms so closely related both appear in set.mm. Indeed, such equalities are generally used in later proofs as parts of transitive inferences, and with the many variants of eqtri 2632 (search for *eqtr*), it would be rare that either one would shorten a proof compared to the other. There is typically a choice between (what we call) a "definitional form" where the shorter expression is on the lhs, and a "computational form" where the shorter expression is on the rhs. An example is df-2 10956 versus 1p1e2 11011. We do not need 1p1e2 11011, but because it occurs "naturally" in computations, it can be useful to have it directly, together with a uniform set of 1-digit operations like 1p2e3 11029, etc. In most cases, we do not need both a definitional and a computational forms. A definitional form would favor consistency with genuine definitions, while a computationa form is often more natural. The situation is similar with biconditionals in propositional calculus: see for instance pm4.24 673 and anidm 674, while other biconditionals generally appear in a single form (either definitional, but more often computational). In the present case, the equality is important enough that both abid1 2731 and abid2 2732 are in set.mm. (Contributed by NM, 26-Dec-1993.) (Revised by BJ, 10-Nov-2020.) |
⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} | ||
Theorem | abid2 2732* | A simplification of class abstraction. Commuted form of abid1 2731. See comments there. (Contributed by NM, 26-Dec-1993.) |
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 | ||
Theorem | cbvab 2733 | Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} | ||
Theorem | cbvabv 2734* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} | ||
Theorem | clelab 2735* | Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) | ||
Theorem | clabel 2736* | Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.) |
⊢ ({𝑥 ∣ 𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))) | ||
Theorem | sbab 2737* | The right-hand side of the second equality is a way of representing proper substitution of 𝑦 for 𝑥 into a class variable. (Contributed by NM, 14-Sep-2003.) |
⊢ (𝑥 = 𝑦 → 𝐴 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐴}) | ||
Syntax | wnfc 2738 | Extend wff definition to include the not-free predicate for classes. |
wff Ⅎ𝑥𝐴 | ||
Theorem | nfcjust 2739* | Justification theorem for df-nfc 2740. (Contributed by Mario Carneiro, 13-Oct-2016.) |
⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴 ↔ ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴) | ||
Definition | df-nfc 2740* | Define the not-free predicate for classes. This is read "𝑥 is not free in 𝐴". Not-free means that the value of 𝑥 cannot affect the value of 𝐴, e.g., any occurrence of 𝑥 in 𝐴 is effectively bound by a "for all" or something that expands to one (such as "there exists"). It is defined in terms of the not-free predicate df-nf 1701 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfci 2741* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 ⇒ ⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcii 2742* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcr 2743* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcrii 2744* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcri 2745* | Consequence of the not-free predicate. (Note that unlike nfcr 2743, this does not require 𝑦 and 𝐴 to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | ||
Theorem | nfcd 2746* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfceqdf 2747 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)) | ||
Theorem | nfceqi 2748 | Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵) | ||
Theorem | nfcxfr 2749 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ 𝐴 = 𝐵 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcxfrd 2750 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfcv 2751* | If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcvd 2752* | If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfab1 2753 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} | ||
Theorem | nfnfc1 2754 | The setvar 𝑥 is bound in Ⅎ𝑥𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥Ⅎ𝑥𝐴 | ||
Theorem | nfab 2755 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} | ||
Theorem | nfaba1 2756 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑} | ||
Theorem | nfcrd 2757* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfeqd 2758 | Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵) | ||
Theorem | nfeld 2759 | Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵) | ||
Theorem | nfnfc 2760 | Hypothesis builder for Ⅎ𝑦𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-13 2234. (Revised by Wolf Lammen, 10-Dec-2019.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Ⅎ𝑦𝐴 | ||
Theorem | nfnfcALT 2761 | Alternate proof of nfnfc 2760. Shorter but requiring more axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Ⅎ𝑦𝐴 | ||
Theorem | nfeq 2762 | Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 = 𝐵 | ||
Theorem | nfel 2763 | Hypothesis builder for elementhood. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | ||
Theorem | nfeq1 2764* | Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝐴 = 𝐵 | ||
Theorem | nfel1 2765* | Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | ||
Theorem | nfeq2 2766* | Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 = 𝐵 | ||
Theorem | nfel2 2767* | Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | ||
Theorem | drnfc1 2768 | Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑦𝐵)) | ||
Theorem | drnfc2 2769 | Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝐴 ↔ Ⅎ𝑧𝐵)) | ||
Theorem | nfabd2 2770 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓}) | ||
Theorem | nfabd 2771 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓}) | ||
Theorem | dvelimdc 2772 | Deduction form of dvelimc 2773. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑧𝐵) & ⊢ (𝜑 → (𝑧 = 𝑦 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵)) | ||
Theorem | dvelimc 2773 | Version of dvelim 2325 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑧𝐵 & ⊢ (𝑧 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵) | ||
Theorem | nfcvf 2774 | If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) | ||
Theorem | nfcvf2 2775 | If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. (Contributed by Mario Carneiro, 5-Dec-2016.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) | ||
Theorem | cleqf 2776 | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2711. (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | abid2f 2777 | A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 5-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 | ||
Theorem | abeq2f 2778 | Equality of a class variable and a class abstraction. In this version, the fact that 𝑥 is a non-free variable in 𝐴 is explicitely stated as a hypothesis. (Contributed by Thierry Arnoux, 11-May-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | sbabel 2779* | Theorem to move a substitution in and out of a class abstraction. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 26-Dec-2019.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ([𝑦 / 𝑥]{𝑧 ∣ 𝜑} ∈ 𝐴 ↔ {𝑧 ∣ [𝑦 / 𝑥]𝜑} ∈ 𝐴) | ||
Syntax | wne 2780 | Extend wff notation to include inequality. |
wff 𝐴 ≠ 𝐵 | ||
Syntax | wnel 2781 | Extend wff notation to include negated membership. |
wff 𝐴 ∉ 𝐵 | ||
Definition | df-ne 2782 | Define inequality. (Contributed by NM, 26-May-1993.) |
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | ||
Definition | df-nel 2783 | Define negated membership. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | ||
Theorem | neii 2784 | Inference associated with df-ne 2782. (Contributed by BJ, 7-Jul-2018.) |
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ ¬ 𝐴 = 𝐵 | ||
Theorem | neir 2785 | Inference associated with df-ne 2782. (Contributed by BJ, 7-Jul-2018.) |
⊢ ¬ 𝐴 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐵 | ||
Theorem | nne 2786 | Negation of inequality. (Contributed by NM, 9-Jun-2006.) |
⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | ||
Theorem | neneqd 2787 | Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 = 𝐵) | ||
Theorem | neneq 2788 | From inequality to non equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) | ||
Theorem | neqned 2789 | If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2787. One-way deduction form of df-ne 2782. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2808. (Revised by Wolf Lammen, 22-Nov-2019.) |
⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | neqne 2790 | From non equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵) | ||
Theorem | neirr 2791 | No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ ¬ 𝐴 ≠ 𝐴 | ||
Theorem | exmidne 2792 | Excluded middle with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 17-Nov-2019.) |
⊢ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵) | ||
Theorem | eqneqall 2793 | A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑)) | ||
Theorem | nonconne 2794 | Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 21-Dec-2019.) |
⊢ ¬ (𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵) | ||
Theorem | necon3ad 2795 | Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) | ||
Theorem | necon3bd 2796 | Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) | ||
Theorem | necon2ad 2797 | Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) | ||
Theorem | necon2bd 2798 | Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.) |
⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) | ||
Theorem | necon1ad 2799 | Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) | ||
Theorem | necon1bd 2800 | Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |