P. 29 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2801-2900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nulmo 2801*	There exists at most one empty set. With either axnul 5212 or axnulALT 5211 or ax-nul 5213, this proves that there exists a unique empty set. In practice, once the language of classes is available, we use the stronger characterization among classes eq0 4311. (Contributed by NM, 22-Dec-2007.) Use the at-most-one quantifier. (Revised by BJ, 17-Sep-2022.) (Proof shortened by Wolf Lammen, 26-Apr-2023.)
⊢ ∃*𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2.1.2  Classes
2.1.2.1  Class abstractions
Syntax	cab 2802	Introduce the class builder or class abstraction notation ("the class of sets 𝑥 such that 𝜑"). Our class variables 𝐴, 𝐵, etc. range over class builders (implicitly in the case of defined class terms such as df-nul 4295). Note that a setvar variable can be expressed as a class builder per theorem cvjust 2819, justifying the assignment of setvar variables to class variables via the use of cv 1535.
class {𝑥 ∣ 𝜑}
Definition	df-clab 2803	Define class abstractions, that is, classes of the form {𝑦 ∣ 𝜑}, which is read "the class of sets 𝑦 such that 𝜑(𝑦)". A few remarks are in order: 1. The axiomatic statement df-clab 2803 does not define the class abstraction {𝑦 ∣ 𝜑} itself, that is, it does not have the form ⊢ {𝑦 ∣ 𝜑} = ... that a standard definition should have (for a good reason: equality itself has not yet been defined or axiomatized for class abstractions; it is defined later in df-cleq 2817). Instead, df-clab 2803 has the form ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ ...), meaning that it only defines what it means for a setvar to be a member of a class abstraction. As a consequence, one can say that df-clab 2803 defines class abstractions if and only if a class abstraction is completely determined by which elements belong to it, which is the content of the axiom of extensionality ax-ext 2796. Therefore, df-clab 2803 can be considered a definition only in systems that can prove ax-ext 2796 (and the necessary first-order logic). 2. As in all definitions, the LHS (definiendum) has no disjoint variable conditions. In particular, the setvar variables 𝑥 and 𝑦 need not be distinct, and the formula 𝜑 may depend on both 𝑥 and 𝑦. This is necessary, as with all definitions, since if there was for instance a disjoint variable condition on 𝑥, 𝑦, then one could not do anything with expressions like 𝑥 ∈ {𝑥 ∣ 𝜑} which are sometimes useful to shorten proofs (because of abid 2806). Most often, however, 𝑥 does not occur in {𝑦 ∣ 𝜑} and 𝑦 is free in 𝜑. 3. Remark 1 stresses that df-clab 2803 does not have the standard form of a definition for a class, but one could be led to think it has the standard form of a definition for a formula. However, it also fails that test since the membership precidate ∈ has already appeared earlier (e.g., in the non-syntactic statement ax-8 2115). Indeed, the LHS extends, or "overloads", the membership predicate ∈ from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This is possible because of wcel 2113 and cab 2802, and it can be called an "extension" of the membership predicate because of wel 2114, whose proof uses cv 1535. An a posteriori justification for cv 1535 is given by cvjust 2819, stating that every setvar can be written as a class abstraction (though conversely not every class abstraction is a set, as illustrated by Russell's paradox ru 3774). 4. Proof techniques. Because class variables can be substituted with compound expressions and setvar variables cannot, it is often useful to convert a theorem containing a free setvar variable to a more general version with a class variable. This is done with theorems such as vtoclg 3570 which is used, for example, to convert elirrv 9063 to elirr 9064. 5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2803, df-cleq 2817, and df-clel 2896, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 28182), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2817 and df-clel 2896). One could be less strict and decide to call "definition" every axiomatic statement which provides an eliminable and conservative extension of the considered axiom system. But the notion of conservativity may be given two different meanings in set.mm, due to the difference between the "scheme level" of set.mm and the "object level" of classical treatments. For a proof that these three axiomatic statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ax-ext 2796, see Appendix of [Levy] p. 357. 6. References and history. The concept of class abstraction dates back to at least Frege, and is used by Whitehead and Russell. This definition is Definition 2.1 of [Quine] p. 16 and Axiom 4.3.1 of [Levy] p. 12. It is called the "axiom of class comprehension" by [Levy] p. 358, who treats the theory of classes as an extralogical extension to predicate logic and set theory axioms. He calls the construction {𝑦 ∣ 𝜑} a "class term". For a full description of how classes are introduced and how to recover the primitive language, see the books of Quine and Levy (and the comment of abeq2 2948 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2948. (Contributed by NM, 26-May-1993.) (Revised by BJ, 19-Aug-2023.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
Theorem	eleq1ab 2804	Extension (in the sense of Remark 3 of the comment of df-clab 2803) of elequ1 2120 from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This extension does not require ax-8 2115 contrary to elequ1 2120, but recall from Remark 3 of the comment of df-clab 2803 that it can be considered an extension only because of cvjust 2819, which does require ax-8 2115. This is an instance of eleq1w 2898 where the containing class is a class abstraction, and contrary to it, it can be proved without df-clel 2896. See also eleq1 2903 for general classes. The straightforward yet important fact that this statement can be proved from FOL= plus df-clab 2803 (hence without ax-ext 2796, df-cleq 2817 or df-clel 2896) was stressed by Mario Carneiro. (Contributed by BJ, 17-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑧 ∣ 𝜑} ↔ 𝑦 ∈ {𝑧 ∣ 𝜑}))
Theorem	cleljustab 2805*	Extension of cleljust 2122 from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This is an instance of dfclel 2897 where the containing class is a class abstraction. The same remarks as for eleq1ab 2804 apply. (Contributed by BJ, 8-Nov-2021.) (Proof shortened by Steven Nguyen, 19-May-2023.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ {𝑦 ∣ 𝜑}))
Theorem	abid 2806	Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993.)
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
Theorem	vexwt 2807	A standard theorem of predicate calculus (stdpc4 2072) expressed using class abstractions. Closed form of vexw 2808. (Contributed by BJ, 14-Jun-2019.)
⊢ (∀𝑥𝜑 → 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	vexw 2808	If 𝜑 is a theorem, then any set belongs to the class {𝑥 ∣ 𝜑}. Therefore, {𝑥 ∣ 𝜑} is "a" universal class. This is the closest one can get to defining a universal class, or proving vex 3500, without using ax-ext 2796. Note that this theorem has no disjoint variable condition and does not use df-clel 2896 nor df-cleq 2817 either: only propositional logic and ax-gen 1795 and df-clab 2803. This is sbt 2070 expressed using class abstractions. Without ax-ext 2796, one cannot define "the" universal class, since one could not prove for instance the justification theorem {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} (see vjust 3498). Indeed, in order to prove any equality of classes, one needs df-cleq 2817, which has ax-ext 2796 as a hypothesis. Therefore, the classes {𝑥 ∣ ⊤}, {𝑦 ∣ (𝜑 → 𝜑)}, {𝑧 ∣ (∀𝑡𝑡 = 𝑡 → ∀𝑡𝑡 = 𝑡)} and countless others are all universal classes whose equality cannot be proved without ax-ext 2796. Once dfcleq 2818 is available, we will define "the" universal class in df-v 3499. Its degenerate instance is also a simple consequence of abid 2806 (using mpbir 233). (Contributed by BJ, 13-Jun-2019.) Reduce axiom dependencies. (Revised by Steven Nguyen, 25-Apr-2023.)
⊢ 𝜑    ⇒   ⊢ 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	vextru 2809	Every setvar is a member of {𝑥 ∣ ⊤}, which is therefore "a" universal class. Once class extensionality dfcleq 2818 is available, we can say "the" universal class (see df-v 3499). This is sbtru 2071 expressed using class abstractions. (Contributed by BJ, 2-Sep-2023.)
⊢ 𝑦 ∈ {𝑥 ∣ ⊤}
Theorem	hbab1 2810*	Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 26-May-1993.)
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → ∀𝑥 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	nfsab1 2811*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove use of ax-12 2176. (Revised by SN, 20-Sep-2023.)
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	nfsab1OLD 2812*	Obsolete version of nfsab1 2811 as of 20-Sep-2023. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	hbab 2813*	Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 1-Mar-1995.) Add disjoint variable condition to avoid ax-13 2389. See hbabg 2814 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} → ∀𝑥 𝑧 ∈ {𝑦 ∣ 𝜑})
Theorem	hbabg 2814*	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2389. See hbab 2813 for a version with more disjoint variable conditions, but not requiring ax-13 2389. (Contributed by NM, 1-Mar-1995.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} → ∀𝑥 𝑧 ∈ {𝑦 ∣ 𝜑})
Theorem	nfsab 2815*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2389. See nfsabg 2816 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
Theorem	nfsabg 2816*	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2389. See nfsab 2815 for a version with more disjoint variable conditions, but not requiring ax-13 2389. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
2.1.2.2  Class equality This section introduces class equality in df-cleq 2817. Note that apart from the local introduction of class variables to state the syntax axioms wceq 1536 and wcel 2113, this section is the first to use class variables. Therefore, the file set.mm contains declarations of class variables at the beginning of this section (not visible on the webpages).
Definition	df-cleq 2817*	Define the equality connective between classes. Definition 2.7 of [Quine] p. 18. Also Definition 4.5 of [TakeutiZaring] p. 13; Chapter 4 provides its justification and methods for eliminating it. Note that its elimination will not necessarily result in a single wff in the original language but possibly a "scheme" of wffs. The hypotheses express that all instances of the conclusion where class variables are replaced with setvar variables hold. Therefore, this definition merely extends to class variables something that is true for setvar variables, hence is conservative. This is only a proof sketch of conservativity; for details see Appendix of [Levy] p. 357. This is the reason why we call this axiomatic statement a "definition", even though it does not have the usual form of a definition. If we required a definition to have the usual form, we would call df-cleq 2817 an axiom. See also comments under df-clab 2803, df-clel 2896, and abeq2 2948. In the form of dfcleq 2818, this is called the "axiom of extensionality" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. While the three class definitions df-clab 2803, df-cleq 2817, and df-clel 2896 are eliminable and conservative and thus meet the requirements for sound definitions, they are technically axioms in that they do not satisfy the requirements for the current definition checker. The proofs of conservativity require external justification that is beyond the scope of the definition checker. For a general discussion of the theory of classes, see mmset.html#class 2896. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.)
⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))    &   ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	dfcleq 2818*	The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2796) and the definition of class equality (df-cleq 2817). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2799 to prove also the hypothesis of df-cleq 2817 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1795, equid 2018 }. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.)
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	cvjust 2819*	Every set is a class. Proposition 4.9 of [TakeutiZaring] p. 13. This theorem shows that a setvar variable can be expressed as a class abstraction. This provides a motivation for the class syntax construction cv 1535, which allows us to substitute a setvar variable for a class variable. See also cab 2802 and df-clab 2803. Note that this is not a rigorous justification, because cv 1535 is used as part of the proof of this theorem, but a careful argument can be made outside of the formalism of Metamath, for example as is done in Chapter 4 of Takeuti and Zaring. See also the discussion under the definition of class in [Jech] p. 4 showing that "Every set can be considered to be a class." See abid1 2959 for the version of cvjust 2819 extended to classes. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2389. (Revised by Wolf Lammen, 4-May-2023.)
⊢ 𝑥 = {𝑦 ∣ 𝑦 ∈ 𝑥}
Theorem	ax9ALT 2820	Proof of ax-9 2123 from Tarski's FOL and dfcleq 2818. For a version not using ax-8 2115 either, see bj-ax9 34220. This shows that dfcleq 2818 is too powerful to be used as a definition instead of df-cleq 2817. Note that ax-ext 2796 is also a direct consequence of dfcleq 2818 (as an instance of its forward implication). (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
Theorem	eqriv 2821*	Infer equality of classes from equivalence of membership. (Contributed by NM, 21-Jun-1993.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)    ⇒   ⊢ 𝐴 = 𝐵
Theorem	eqrdv 2822*	Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqrdav 2823*	Deduce equality of classes from an equivalence of membership that depends on the membership variable. (Contributed by NM, 7-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqid 2824	Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine] p. 41. This is part of Frege's eighth axiom per Proposition 54 of [Frege1879] p. 50; see also biid 263. An early mention of this law can be found in Aristotle, Metaphysics, Z.17, 1041a10-20. (Thanks to Stefan Allan and BJ for this information.) (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 14-Oct-2017.)
⊢ 𝐴 = 𝐴
Theorem	eqidd 2825	Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
⊢ (𝜑 → 𝐴 = 𝐴)
Theorem	eqeq1d 2826	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq1dALT 2827	Shorter proof of eqeq1d 2826 based on more axioms. (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen, 19-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq1 2828	Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq1i 2829	Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
Theorem	eqcomd 2830	Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.) Allow shortening of eqcom 2831. (Revised by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐴)
Theorem	eqcom 2831	Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
Theorem	eqcoms 2832	Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 24-Jun-1993.)
⊢ (𝐴 = 𝐵 → 𝜑)    ⇒   ⊢ (𝐵 = 𝐴 → 𝜑)
Theorem	eqcomi 2833	Inference from commutative law for class equality. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 = 𝐴
Theorem	neqcomd 2834	Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐵 = 𝐴)
Theorem	eqeq2d 2835	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) Allow shortening of eqeq2 2836. (Revised by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
Theorem	eqeq2 2836	Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
Theorem	eqeq2i 2837	Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)
Theorem	eqeq12 2838	Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeq12i 2839	A useful inference for substituting definitions into an equality. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)
Theorem	eqeq12d 2840	A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeqan12d 2841	A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2842. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeqan12dALT 2842	Alternate proof of eqeqan12d 2841. This proof has one more step but one fewer essential step. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeqan12rd 2843	A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqtr 2844	Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
Theorem	eqtr2 2845	A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)
Theorem	eqtr3 2846	A transitive law for class equality. (Contributed by NM, 20-May-2005.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
Theorem	eqtri 2847	An equality transitivity inference. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 = 𝐶
Theorem	eqtr2i 2848	An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐶 = 𝐴
Theorem	eqtr3i 2849	An equality transitivity inference. (Contributed by NM, 6-May-1994.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    ⇒   ⊢ 𝐵 = 𝐶
Theorem	eqtr4i 2850	An equality transitivity inference. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 = 𝐶
Theorem	3eqtri 2851	An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐴 = 𝐷
Theorem	3eqtrri 2852	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐷 = 𝐴
Theorem	3eqtr2i 2853	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐴 = 𝐷
Theorem	3eqtr2ri 2854	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐷 = 𝐴
Theorem	3eqtr3i 2855	An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐶 = 𝐷
Theorem	3eqtr3ri 2856	An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐷 = 𝐶
Theorem	3eqtr4i 2857	An inference from three chained equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐶 = 𝐷
Theorem	3eqtr4ri 2858	An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐷 = 𝐶
Theorem	eqtrd 2859	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2d 2860	An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr3d 2861	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	eqtr4d 2862	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	3eqtrd 2863	A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐷)
Theorem	3eqtrrd 2864	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐴)
Theorem	3eqtr2d 2865	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐷)
Theorem	3eqtr2rd 2866	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐴)
Theorem	3eqtr3d 2867	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr3rd 2868	A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	3eqtr4d 2869	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4rd 2870	A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	syl5eq 2871	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	syl5req 2872	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	syl5eqr 2873	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	syl5reqr 2874	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	syl6eq 2875	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	syl6req 2876	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	syl6eqr 2877	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	syl6reqr 2878	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	sylan9eq 2879	An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
Theorem	sylan9req 2880	An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
Theorem	sylan9eqr 2881	An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)
Theorem	3eqtr3g 2882	A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr3a 2883	A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4g 2884	A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4a 2885	A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	eq2tri 2886	A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
⊢ (𝐴 = 𝐶 → 𝐷 = 𝐹)    &   ⊢ (𝐵 = 𝐷 → 𝐶 = 𝐺)    ⇒   ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐹) ↔ (𝐵 = 𝐷 ∧ 𝐴 = 𝐺))
Theorem	abbi1 2887	Equivalent formulas yield equal class abstractions (closed form). This is the forward implication of abbi 2891, proved from fewer axioms. (Contributed by BJ and WL and SN, 20-Aug-2023.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
Theorem	abbidv 2888*	Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2176, based on an idea of Steven Nguyen. (Revised by Wolf Lammen, 6-May-2023.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	abbii 2889	Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2144, ax-11 2160, and ax-12 2176. (Revised by Steven Nguyen, 3-May-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}
Theorem	abbid 2890	Equivalent wff's yield equal class abstractions (deduction form, with nonfreeness hypothesis). (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) Avoid ax-10 2144 and ax-11 2160. (Revised by Wolf Lammen, 6-May-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	abbi 2891	Equivalent formulas define equal class abstractions, and conversely. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-8 2115 and df-clel 2896 (by avoiding use of cleqh 2939). (Revised by BJ, 23-Jun-2019.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
Theorem	cbvabv 2892*	Rule used to change bound variables, using implicit substitution. Version of cbvab 2894 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2160 and ax-13 2389. (Revised by Steven Nguyen, 4-Dec-2022.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	cbvabw 2893*	Rule used to change bound variables, using implicit substitution. Version of cbvab 2894 with a disjoint variable condition, which does not require ax-13 2389. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	cbvab 2894	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2389. Usage of the weaker cbvabw 2893 and cbvabv 2892 are preferred. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	cbvabvOLD 2895*	Obsolete version of cbvabv 2892 as of 9-May-2023. (Contributed by NM, 26-May-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
2.1.2.3  Class membership
Definition	df-clel 2896*	Define the membership connective between classes. Theorem 6.3 of [Quine] p. 41, or Proposition 4.6 of [TakeutiZaring] p. 13, which we adopt as a definition. See these references for its metalogical justification. The hypotheses express that all instances of the conclusion where class variables are replaced with setvar variables hold. Therefore, this definition merely extends to class variables something that is true for setvar variables, hence is conservative. This is only a proof sketch of conservativity; for details see Appendix of [Levy] p. 357. This is the reason why we call this axiomatic statement a "definition", even though it does not have the usual form of a definition. If we required a definition to have the usual form, we would call df-clel 2896 an axiom. See also comments under df-clab 2803, df-cleq 2817, and abeq2 2948. Alternate characterizations of 𝐴 ∈ 𝐵 when either 𝐴 or 𝐵 is a set are given by clel2 3656, clel3 3658, and clel4 3659. This is called the "axiom of membership" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. While the three class definitions df-clab 2803, df-cleq 2817, and df-clel 2896 are eliminable and conservative and thus meet the requirements for sound definitions, they are technically axioms in that they do not satisfy the requirements for the current definition checker. The proofs of conservativity require external justification that is beyond the scope of the definition checker. For a general discussion of the theory of classes, see mmset.html#class 2896. (Contributed by NM, 26-May-1993.) (Revised by BJ, 27-Jun-2019.)
⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))    &   ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	dfclel 2897*	Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019.)
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	eleq1w 2898	Weaker version of eleq1 2903 (but more general than elequ1 2120) not depending on ax-ext 2796 nor df-cleq 2817. Note that this provides a proof of ax-8 2115 from Tarski's FOL and dfclel 2897 (simply consider an instance where 𝐴 is replaced by a setvar and deduce the forward implication by biimpd 231), which shows that dfclel 2897 is too powerful to be used as a definition instead of df-clel 2896. (Contributed by BJ, 24-Jun-2019.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
Theorem	eleq2w 2899	Weaker version of eleq2 2904 (but more general than elequ2 2128) not depending on ax-ext 2796 nor df-cleq 2817. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))
Theorem	eleq1d 2900	Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) Allow shortening of eleq1 2903. (Revised by Wolf Lammen, 20-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))