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