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