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	eqabbw 2801*	Version of eqabb 2865 using implicit substitution, which requires fewer axioms. (Contributed by GG and AV, 18-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝜓))
2.1.2.3  Class membership
Definition	df-clel 2802*	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 2802 an axiom. See also comments under df-clab 2703, df-cleq 2717, and eqabb 2865. Alternate characterizations of 𝐴 ∈ 𝐵 when either 𝐴 or 𝐵 is a set are given by clel2g 3642, clel3g 3645, and clel4g 3647. 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 2703, df-cleq 2717, and df-clel 2802 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 2802. (Contributed by NM, 26-May-1993.) (Revised by BJ, 27-Jun-2019.)
⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))    &   ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	dfclel 2803*	Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019.)
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	elex2 2804*	If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.) Avoid ax-9 2108, ax-ext 2696, df-clab 2703. (Revised by Wolf Lammen, 30-Nov-2024.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)
Theorem	issetlem 2805*	Lemma for elisset 2807 and isset 3474. (Contributed by NM, 26-May-1993.) Extract from the proof of isset 3474. (Revised by WL, 2-Feb-2025.)
⊢ 𝑥 ∈ 𝑉    ⇒   ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑥 𝑥 = 𝐴)
Theorem	elissetv 2806*	An element of a class exists. Version of elisset 2807 with a disjoint variable condition on 𝑉, 𝑥, avoiding df-clab 2703. Prefer its use over elisset 2807 when sufficient (for instance in usages where 𝑥 is a dummy variable). (Contributed by BJ, 14-Sep-2019.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
Theorem	elisset 2807*	An element of a class exists. Use elissetv 2806 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 2808	Weaker version of eleq1 2813 (but more general than elequ1 2105) not depending on ax-ext 2696 nor df-cleq 2717. Note that this provides a proof of ax-8 2100 from Tarski's FOL and dfclel 2803 (simply consider an instance where 𝐴 is replaced by a setvar and deduce the forward implication by biimpd 228), which shows that dfclel 2803 is too powerful to be used as a definition instead of df-clel 2802. (Contributed by BJ, 24-Jun-2019.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
Theorem	eleq2w 2809	Weaker version of eleq2 2814 (but more general than elequ2 2113) not depending on ax-ext 2696 nor df-cleq 2717. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))
Theorem	eleq1d 2810	Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) Allow shortening of eleq1 2813. (Revised by Wolf Lammen, 20-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
Theorem	eleq2d 2811	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 2812	Alternate proof of eleq2d 2811, shorter at the expense of requiring ax-12 2166. (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen, 20-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
Theorem	eleq1 2813	Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
Theorem	eleq2 2814	Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
Theorem	eleq12 2815	Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))
Theorem	eleq1i 2816	Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
Theorem	eleq2i 2817	Inference from equality to equivalence of membership. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)
Theorem	eleq12i 2818	Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)
Theorem	eleq12d 2819	Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))
Theorem	eleq1a 2820	A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))
Theorem	eqeltri 2821	Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ 𝐴 ∈ 𝐶
Theorem	eqeltrri 2822	Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ 𝐵 ∈ 𝐶
Theorem	eleqtri 2823	Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 ∈ 𝐶
Theorem	eleqtrri 2824	Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 ∈ 𝐶
Theorem	eqeltrd 2825	Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrrd 2826	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝐶)
Theorem	eleqtrd 2827	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrrd 2828	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrid 2829	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrrid 2830	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrid 2831	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrrid 2832	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrdi 2833	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrrdi 2834	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrdi 2835	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrrdi 2836	A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	3eltr3i 2837	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐶 ∈ 𝐷
Theorem	3eltr4i 2838	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐶 ∈ 𝐷
Theorem	3eltr3d 2839	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	3eltr4d 2840	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	3eltr3g 2841	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	3eltr4g 2842	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	eleq2s 2843	Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝐴 ∈ 𝐵 → 𝜑)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝐴 ∈ 𝐶 → 𝜑)
Theorem	eqneltri 2844	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 2845	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 2846	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 2847	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 2848	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 2849	A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.)
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵)
Theorem	nelneq2 2850	A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶)
Theorem	eqsb1 2851*	Substitution for the left-hand side in an equality. Class version of equsb3 2093. (Contributed by Rodolfo Medina, 28-Apr-2010.)
⊢ ([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴)
Theorem	clelsb1 2852*	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2106). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
Theorem	clelsb2 2853*	Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 2115). (Contributed by Jim Kingdon, 22-Nov-2018.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 24-Nov-2024.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)
Theorem	clelsb2OLD 2854*	Obsolete version of clelsb2 2853 as of 24-Nov-2024.) (Contributed by Jim Kingdon, 22-Nov-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)
Theorem	cleqh 2855*	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions as in dfcleq 2718. See also cleqf 2923. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2019.) Remove dependency on ax-13 2365. (Revised by BJ, 30-Nov-2020.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    &   ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	hbxfreq 2856	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1819 for equivalence version. (Contributed by NM, 21-Aug-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵)    ⇒   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
Theorem	hblem 2857*	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 2365. See hblemg 2858 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴)
Theorem	hblemg 2858*	Change the free variable of a hypothesis builder. Usage of this theorem is discouraged because it depends on ax-13 2365. See hblem 2857 for a version with more disjoint variable conditions, but not requiring ax-13 2365. (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 2859*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) Avoid ax-11 2146. (Revised by Wolf Lammen, 6-May-2023.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
Theorem	eqabcdv 2860*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)
Theorem	eqabi 2861*	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2146. (Revised by Wolf Lammen, 6-May-2023.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)    ⇒   ⊢ 𝐴 = {𝑥 ∣ 𝜑}
Theorem	abid1 2862*	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 2719. The proof does not rely on cvjust 2719, so cvjust 2719 could be proved as a special instance of it. Note however that abid1 2862 necessarily relies on df-clel 2802, whereas cvjust 2719 does not. This theorem requires ax-ext 2696, df-clab 2703, df-cleq 2717, df-clel 2802, 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 1532, cab 2702, and statements corresponding to defined class constructors. Note on the simultaneous presence in set.mm of this abid1 2862 and its commuted form abid2 2863: 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 2753 (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 12308 versus 1p1e2 12370. We do not need 1p1e2 12370, 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 12388, 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 562 and anidm 563, 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 2862 and abid2 2863 are in set.mm. (Contributed by NM, 26-Dec-1993.) (Revised by BJ, 10-Nov-2020.)
⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
Theorem	abid2 2863*	A simplification of class abstraction. Commuted form of abid1 2862. See comments there. (Contributed by NM, 26-Dec-1993.)
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
Theorem	eqab 2864*	One direction of eqabb 2865 is provable from fewer axioms. (Contributed by Wolf Lammen, 13-Feb-2025.)
⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑) → 𝐴 = {𝑥 ∣ 𝜑})
Theorem	eqabb 2865*	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 2797 and its relatives are among those useful for converting theorems with class variables to equivalent theorems with wff variables, by first substituting a class abstraction for each class variable. Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable 𝜑 (that has a free variable 𝑥) to a theorem with a class variable 𝐴, we substitute 𝑥 ∈ 𝐴 for 𝜑 throughout and simplify, where 𝐴 is a new class variable not already in the wff. An example is the conversion of zfauscl 5302 to inex1 5318 (look at the instance of zfauscl 5302 that occurs in the proof of inex1 5318). 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 4249 and cp 9916; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 9915. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. Usage of eqabbw 2801 is preferred since it requires fewer axioms. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2025.)
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))
Theorem	eqabbOLD 2866*	Obsolete version of eqabb 2865 as of 12-Feb-2025. (Contributed by NM, 26-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))
Theorem	eqabcb 2867*	Equality of a class variable and a class abstraction. Commuted form of eqabb 2865. (Contributed by NM, 20-Aug-1993.)
⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝑥 ∈ 𝐴))
Theorem	eqabrd 2868	Equality of a class variable and a class abstraction (deduction form of eqabb 2865). (Contributed by NM, 16-Nov-1995.)
⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))
Theorem	eqabri 2869	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.) (Proof shortened by Wolf Lammen, 15-Nov-2019.)
⊢ 𝐴 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)
Theorem	eqabcri 2870	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 31-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Nov-2019.)
⊢ {𝑥 ∣ 𝜑} = 𝐴    ⇒   ⊢ (𝜑 ↔ 𝑥 ∈ 𝐴)
Theorem	clelab 2871*	Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) Avoid ax-11 2146, see sbc5ALT 3802 for more details. (Revised by SN, 2-Sep-2024.)
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
Theorem	clelabOLD 2872*	Obsolete version of clelab 2871 as of 2-Sep-2024. (Contributed by NM, 23-Dec-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
Theorem	clabel 2873*	Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.)
⊢ ({𝑥 ∣ 𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑)))
Theorem	sbab 2874*	The right-hand side of the second equality is a way of representing proper substitution of 𝑦 for 𝑥 into a class variable. (Contributed by NM, 14-Sep-2003.)
⊢ (𝑥 = 𝑦 → 𝐴 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐴})
2.1.3  Class form not-free predicate
Syntax	wnfc 2875	Extend wff definition to include the not-free predicate for classes.
wff Ⅎ𝑥𝐴
Theorem	nfcjust 2876*	Justification theorem for df-nfc 2877. (Contributed by Mario Carneiro, 13-Oct-2016.)
⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴 ↔ ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴)
Definition	df-nfc 2877*	Define the not-free predicate for classes. This is read "𝑥 is not free in 𝐴". Not-free means that the value of 𝑥 cannot affect the value of 𝐴, e.g., any occurrence of 𝑥 in 𝐴 is effectively bound by a "for all" or something that expands to one (such as "there exists"). It is defined in terms of the not-free predicate df-nf 1778 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfci 2878*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥 𝑦 ∈ 𝐴    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcii 2879*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcr 2880*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Drop ax-12 2166 but use ax-8 2100, df-clel 2802, and avoid a DV condition on 𝑦, 𝐴. (Revised by SN, 3-Jun-2024.)
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfcrALT 2881*	Alternate version of nfcr 2880. Avoids ax-8 2100 but uses ax-12 2166. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfcri 2882*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2129, ax-11 2146. (Revised by GG, 23-May-2024.) Avoid ax-12 2166 (adopting Wolf Lammen's 13-May-2023 proof). (Revised by SN, 3-Jun-2024.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
Theorem	nfcd 2883*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfcrd 2884*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfcrii 2885*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2129, ax-11 2146. (Revised by GG, 23-May-2024.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
Theorem	nfceqdf 2886	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.) Avoid ax-8 2100 and df-clel 2802. (Revised by WL and SN, 23-Aug-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵))
Theorem	nfceqdfOLD 2887	Obsolete version of nfceqdf 2886 as of 23-Aug-2024. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵))
Theorem	nfceqi 2888	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) Avoid ax-12 2166. (Revised by Wolf Lammen, 19-Jun-2023.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
Theorem	nfcxfr 2889	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcxfrd 2890	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfcv 2891*	If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴
Theorem	nfcvd 2892*	If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfab1 2893	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
Theorem	nfnfc1 2894	The setvar 𝑥 is bound in Ⅎ𝑥𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥Ⅎ𝑥𝐴
Theorem	clelsb1fw 2895*	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2106). Version of clelsb1f 2896 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by Rodolfo Medina, 28-Apr-2010.) Avoid ax-13 2365. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
Theorem	clelsb1f 2896	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2106). Usage of this theorem is discouraged because it depends on ax-13 2365. See clelsb1fw 2895 not requiring ax-13 2365, but extra disjoint variables. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.) (Proof shortened by Wolf Lammen, 7-May-2023.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
Theorem	nfab 2897*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2365. See nfabg 2898 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}
Theorem	nfabg 2898	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2365. See nfab 2897 for a version with more disjoint variable conditions, but not requiring ax-13 2365. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}
Theorem	nfaba1 2899*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2365. See nfaba1g 2901 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.) Avoid ax-6 1963, ax-7 2003, ax-12 2166. (Revised by SN, 14-May-2025.)
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑}
Theorem	nfaba1OLD 2900*	Obsolete version of nfaba1 2899 as of 14-May-2025. (Contributed by Mario Carneiro, 14-Oct-2016.) (Revised by GG, 20-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑}