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	3eqtr2d 2801	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐷)
Theorem	3eqtr2rd 2802	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐴)
Theorem	3eqtr3d 2803	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr3rd 2804	A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	3eqtr4d 2805	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4rd 2806	A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	eqtrid 2807	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2id 2808	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr3id 2809	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr3di 2810	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐴 = 𝐶    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	eqtrdi 2811	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2di 2812	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr4di 2813	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr4id 2814	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	sylan9eq 2815	An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
Theorem	sylan9req 2816	An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
Theorem	sylan9eqr 2817	An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)
Theorem	3eqtr3g 2818	A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr3a 2819	A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4g 2820	A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4a 2821	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 2822	A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
⊢ (𝐴 = 𝐶 → 𝐷 = 𝐹)    &   ⊢ (𝐵 = 𝐷 → 𝐶 = 𝐺)    ⇒   ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐹) ↔ (𝐵 = 𝐷 ∧ 𝐴 = 𝐺))
Theorem	iseqsetvlem 2823*	Lemma for iseqsetv-cleq 2824. (Contributed by Wolf Lammen, 17-Aug-2025.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑧 𝑧 = 𝐴)
Theorem	iseqsetv-cleq 2824*	Alternate proof of iseqsetv-clel 2839. The expression ∃𝑥𝑥 = 𝐴 does not depend on a particular choice of the set variable. The proof here avoids df-clab 2739, df-clel 2835 and ax-8 2147, but instead is based on ax-9 2155, ax-ext 2732 and df-cleq 2752. In particular it still accepts 𝑥 ∈ 𝐴 being a primitive syntax term, not assuming any specific semantics (like elementhood in some form). Use it in contexts where you want to avoid df-clab 2739, or you need df-cleq 2752 anyway. See the alternative version , not using df-cleq 2752 or ax-ext 2732 or ax-9 2155. (Contributed by Wolf Lammen, 6-Aug-2025.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	abbi 2825	Equivalent formulas yield equal class abstractions (closed form). This is the backward implication of abbib 2829, proved from fewer axioms, and hence is independently named. (Contributed by BJ and WL and SN, 20-Aug-2023.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
Theorem	abbidv 2826*	Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2213, based on an idea of Steven Nguyen. (Revised by Wolf Lammen, 6-May-2023.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	abbii 2827	Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2178, ax-11 2194, and ax-12 2213. (Revised by Steven Nguyen, 3-May-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}
Theorem	abbid 2828	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 2178 and ax-11 2194. (Revised by Wolf Lammen, 6-May-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	abbib 2829	Equal class abstractions require equivalent formulas, and conversely. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-8 2147 and df-clel 2835 (by avoiding use of cleqh 2889). (Revised by BJ, 23-Jun-2019.) Definitial form. (Revised by Wolf Lammen, 23-Feb-2025.)
⊢ ({𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 ↔ 𝜓))
Theorem	cbvabv 2830*	Rule used to change bound variables, using implicit substitution. Version of cbvab 2832 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2194 and ax-13 2401. (Revised by Steven Nguyen, 4-Dec-2022.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	cbvabw 2831*	Rule used to change bound variables, using implicit substitution. Version of cbvab 2832 with a disjoint variable condition, which does not require ax-10 2178, ax-13 2401. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by GG, 23-May-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	cbvab 2832	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2401. Usage of the weaker cbvabw 2831 and cbvabv 2830 are preferred. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	eqabbw 2833*	Version of eqabb 2899 using implicit substitution, which requires fewer axioms. (Contributed by GG and AV, 18-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝜓))
Theorem	eqabcbw 2834*	Version of eqabcb 2900 using implicit substitution, which requires fewer axioms. (Contributed by TM, 24-Jan-2026.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑦(𝜓 ↔ 𝑦 ∈ 𝐴))
2.1.2.3  Class membership
Definition	df-clel 2835*	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 2835 an axiom. See also comments under df-clab 2739, df-cleq 2752, and eqabb 2899. Alternate characterizations of 𝐴 ∈ 𝐵 when either 𝐴 or 𝐵 is a set are given by clel2g 3612, clel3g 3614, and clel4g 3616. 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 2739, df-cleq 2752, and df-clel 2835 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 2835. (Contributed by NM, 26-May-1993.) (Revised by BJ, 27-Jun-2019.)
⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))    &   ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	dfclel 2836*	Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019.)
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	elex2 2837*	If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.) Avoid ax-9 2155, ax-ext 2732, df-clab 2739. (Revised by Wolf Lammen, 30-Nov-2024.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)
Theorem	issettru 2838*	Weak version of isset 3464. (Contributed by BJ, 24-Apr-2024.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	iseqsetv-clel 2839*	Alternate proof of iseqsetv-cleq 2824. The expression ∃𝑥𝑥 = 𝐴 does not depend on a particular choice of the set variable. Use this theorem in contexts where df-cleq 2752 or ax-ext 2732 is not referenced elsewhere in your proof. It is proven from a specific implementation (class builder, axiom df-clab 2739) of the primitive term 𝑥 ∈ 𝐴. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	issetlem 2840*	Lemma for elisset 2842 and isset 3464. (Contributed by NM, 26-May-1993.) Extract from the proof of isset 3464. (Revised by WL, 2-Feb-2025.)
⊢ 𝑥 ∈ 𝑉    ⇒   ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑥 𝑥 = 𝐴)
Theorem	elissetv 2841*	An element of a class exists. Version of elisset 2842 with a disjoint variable condition on 𝑉, 𝑥, avoiding df-clab 2739. Prefer its use over elisset 2842 when sufficient (for instance in usages where 𝑥 is a dummy variable). (Contributed by BJ, 14-Sep-2019.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
Theorem	elisset 2842*	An element of a class exists. Use elissetv 2841 instead when sufficient (for instance in usages where 𝑥 is a dummy variable). (Contributed by NM, 1-May-1995.) Reduce dependencies on axioms. (Revised by BJ, 29-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
Theorem	eleq1w 2843	Weaker version of eleq1 2848 (but more general than elequ1 2152) not depending on ax-ext 2732 nor df-cleq 2752. Note that this provides a proof of ax-8 2147 from Tarski's FOL and dfclel 2836 (simply consider an instance where 𝐴 is replaced by a setvar and deduce the forward implication by biimpd 232), which shows that dfclel 2836 is too powerful to be used as a definition instead of df-clel 2835. (Contributed by BJ, 24-Jun-2019.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
Theorem	eleq2w 2844	Weaker version of eleq2 2849 (but more general than elequ2 2160) not depending on ax-ext 2732 nor df-cleq 2752. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))
Theorem	eleq1d 2845	Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) Allow shortening of eleq1 2848. (Revised by Wolf Lammen, 20-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
Theorem	eleq2d 2846	Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
Theorem	eleq2dALT 2847	Alternate proof of eleq2d 2846, shorter at the expense of requiring ax-12 2213. (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen, 20-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
Theorem	eleq1 2848	Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
Theorem	eleq2 2849	Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
Theorem	eleq12 2850	Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))
Theorem	eleq1i 2851	Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
Theorem	eleq2i 2852	Inference from equality to equivalence of membership. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)
Theorem	eleq12i 2853	Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)
Theorem	eleq12d 2854	Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))
Theorem	eleq1a 2855	A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))
Theorem	eqeltri 2856	Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ 𝐴 ∈ 𝐶
Theorem	eqeltrri 2857	Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ 𝐵 ∈ 𝐶
Theorem	eleqtri 2858	Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 ∈ 𝐶
Theorem	eleqtrri 2859	Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 ∈ 𝐶
Theorem	eqeltrd 2860	Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrrd 2861	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝐶)
Theorem	eleqtrd 2862	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrrd 2863	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrid 2864	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrrid 2865	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrid 2866	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrrid 2867	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrdi 2868	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrrdi 2869	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrdi 2870	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrrdi 2871	A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	3eltr3i 2872	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐶 ∈ 𝐷
Theorem	3eltr4i 2873	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐶 ∈ 𝐷
Theorem	3eltr3d 2874	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	3eltr4d 2875	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	3eltr3g 2876	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	3eltr4g 2877	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	eleq2s 2878	Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝐴 ∈ 𝐵 → 𝜑)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝐴 ∈ 𝐶 → 𝜑)
Theorem	eqneltri 2879	If a class is not an element of another class, an equal class is also not an element. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝐴 = 𝐵    &   ⊢ ¬ 𝐵 ∈ 𝐶    ⇒   ⊢ ¬ 𝐴 ∈ 𝐶
Theorem	eqneltrd 2880	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 2881	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 2882	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 2883	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	nelneq 2884	A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.)
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵)
Theorem	nelneq2 2885	A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶)
Theorem	eqsb1 2886*	Substitution for the left-hand side in an equality. Class version of equsb3 2140. (Contributed by Rodolfo Medina, 28-Apr-2010.)
⊢ ([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴)
Theorem	clelsb1 2887*	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2153). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
Theorem	clelsb2 2888*	Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 2162). (Contributed by Jim Kingdon, 22-Nov-2018.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 24-Nov-2024.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)
Theorem	cleqh 2889*	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions as in dfcleq 2753. See also cleqf 2950. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2019.) Remove dependency on ax-13 2401. (Revised by BJ, 30-Nov-2020.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    &   ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	hbxfreq 2890	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1858 for equivalence version. (Contributed by NM, 21-Aug-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵)    ⇒   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
Theorem	hblem 2891*	Change the free variable of a hypothesis builder. (Contributed by NM, 21-Jun-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) Add disjoint variable condition to avoid ax-13 2401. See hblemg 2892 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴)
Theorem	hblemg 2892*	Change the free variable of a hypothesis builder. Usage of this theorem is discouraged because it depends on ax-13 2401. See hblem 2891 for a version with more disjoint variable conditions, but not requiring ax-13 2401. (Contributed by NM, 21-Jun-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) (New usage is discouraged.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴)
2.1.2.4  Elementary properties of class abstractions
Theorem	eqabdv 2893*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) Avoid ax-11 2194. (Revised by Wolf Lammen, 6-May-2023.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
Theorem	eqabcdv 2894*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)
Theorem	eqabi 2895*	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2194. (Revised by Wolf Lammen, 6-May-2023.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)    ⇒   ⊢ 𝐴 = {𝑥 ∣ 𝜑}
Theorem	abid1 2896*	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 2754. The proof does not rely on cvjust 2754, so cvjust 2754 could be proved as a special instance of it. Note however that abid1 2896 necessarily relies on df-clel 2835, whereas cvjust 2754 does not. This theorem requires ax-ext 2732, df-clab 2739, df-cleq 2752, df-clel 2835, but to prove that any specific class term not containing class variables is a setvar or 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 1569, cab 2738, and statements corresponding to defined class constructors. Note on the simultaneous presence in set.mm of this abid1 2896 and its commuted form abid2 2897: 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 2783 (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 (left-hand side), and a "computational form", where the shorter expression is on the RHS (right-hand side). An example is df-2 12375 versus 1p1e2 12436. We do not need 1p1e2 12436, 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 12455, 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 computational form is often more natural. The situation is similar with biconditionals in propositional calculus: see for instance pm4.24 574 and anidm 575, 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 2896 and abid2 2897 are in set.mm. (Contributed by NM, 26-Dec-1993.) (Revised by BJ, 10-Nov-2020.)
⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
Theorem	abid2 2897*	A simplification of class abstraction. Commuted form of abid1 2896. See comments there. (Contributed by NM, 26-Dec-1993.)
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
Theorem	eqab 2898*	One direction of eqabb 2899 is provable from fewer axioms. (Contributed by Wolf Lammen, 13-Feb-2025.)
⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑) → 𝐴 = {𝑥 ∣ 𝜑})
Theorem	eqabb 2899*	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 abbib 2829 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 sepgi 5251 to inex1 5276 (look at the instance of sepgi 5251 that occurs in the proof of inex1 5276). 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 4206 and cp 9926; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 9924. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. Usage of eqabbw 2833 is preferred since it requires fewer axioms. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2025.)
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))
Theorem	eqabcb 2900*	Equality of a class variable and a class abstraction. Commuted form of eqabb 2899. (Contributed by NM, 20-Aug-1993.)
⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝑥 ∈ 𝐴))