P. 28 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2701-2800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axi9 2701	Axiom of existence (intuitionistic logic axiom ax-i9). In classical logic, this is equivalent to ax-6 1968 but in intuitionistic logic it needs to be stated using the existential quantifier. (Contributed by Jim Kingdon, 31-Dec-2017.) (New usage is discouraged.)
⊢ ∃𝑥 𝑥 = 𝑦
Theorem	axi10 2702	Axiom of Quantifier Substitution (intuitionistic logic axiom ax-10). This is just axc11n 2428 by another name. (Contributed by Jim Kingdon, 31-Dec-2017.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	axi12 2703	Axiom of Quantifier Introduction (intuitionistic logic axiom ax-i12). In classical logic, this is mostly a restatement of axc9 2384 (with one additional quantifier). But in intuitionistic logic, changing the negations and implications to disjunctions makes it stronger. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by Jim Kingdon, 31-Dec-2017.) Avoid ax-11 2162. (Revised by Wolf Lammen, 24-Apr-2023.) (New usage is discouraged.)
⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Theorem	axbnd 2704	Axiom of Bundling (intuitionistic logic axiom ax-bnd). In classical logic, this and axi12 2703 are fairly straightforward consequences of axc9 2384. But in intuitionistic logic, it is not easy to add the extra ∀𝑥 to axi12 2703 and so we treat the two as separate axioms. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by Jim Kingdon, 22-Mar-2018.) (Proof shortened by Wolf Lammen, 24-Apr-2023.) (New usage is discouraged.)
⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
PART 2  ZF (ZERMELO-FRAENKEL) SET THEORY Set theory uses the formalism of propositional and predicate calculus to assert properties of arbitrary mathematical objects called "sets". A set can be an element of another set, and this relationship is indicated by the ∈ symbol. Starting with the simplest mathematical object, called the empty set, set theory builds up more and more complex structures whose existence follows from the axioms, eventually resulting in extremely complicated sets that we identify with the real numbers and other familiar mathematical objects. A simplistic concept of sets, sometimes called "naive set theory", is vulnerable to a paradox called "Russell's Paradox" (ru 3736), a discovery that revolutionized the foundations of mathematics and logic. Russell's Paradox spawned the development of set theories that countered the paradox, including the ZF set theory that is most widely used and is defined here. Except for Extensionality, the axioms basically say, "given an arbitrary set x (and, in the cases of Replacement and Regularity, provided that an antecedent is satisfied), there exists another set y based on or constructed from it, with the stated properties". (The axiom of extensionality can also be restated this way as shown by axexte 2706.) The individual axiom links provide more detailed descriptions. We derive the redundant ZF axioms of Separation, Null Set, and Pairing from the others as theorems.
2.1  ZF Set Theory - start with the Axiom of Extensionality
2.1.1  Introduce the Axiom of Extensionality
Axiom	ax-ext 2705*	Axiom of extensionality. An axiom of Zermelo-Fraenkel set theory. It states that two sets are identical if they contain the same elements. Axiom Ext of [BellMachover] p. 461. Its converse is a theorem of predicate logic, elequ2g 2129. Set theory can also be formulated with a single primitive predicate ∈ on top of traditional predicate calculus without equality. In that case the Axiom of Extensionality becomes (∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)), and equality 𝑥 = 𝑦 is defined as ∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦). All of the usual axioms of equality then become theorems of set theory. See, for example, Axiom 1 of [TakeutiZaring] p. 8. To use the above "equality-free" version of Extensionality with Metamath's predicate calculus axioms, we would rewrite all axioms involving equality with equality expanded according to the above definition. Some of those axioms may be provable from ax-ext and would become redundant, but this hasn't been studied carefully. General remarks: Our set theory axioms are presented using defined connectives (↔, ∃, etc.) for convenience. However, it is implicitly understood that the actual axioms use only the primitive connectives →, ¬, ∀, =, and ∈. It is straightforward to establish the equivalence between the actual axioms and the ones we display, and we will not do so. It is important to understand that strictly speaking, all of our set theory axioms are really schemes that represent an infinite number of actual axioms. This is inherent in the design of Metamath ("metavariable math"), which manipulates only metavariables. For example, the metavariable 𝑥 in ax-ext 2705 can represent any actual variable v1, v2, v3,... . Distinct variable restrictions ($d) prevent us from substituting say v1 for both 𝑥 and 𝑧. This is in contrast to typical textbook presentations that present actual axioms (except for Replacement ax-rep 5221, which involves a wff metavariable). In practice, though, the theorems and proofs are essentially the same. The $d restrictions make each of the infinite axioms generated by the ax-ext 2705 scheme exactly logically equivalent to each other and in particular to the actual axiom of the textbook version. (Contributed by NM, 21-May-1993.)
⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
Theorem	axexte 2706*	The axiom of extensionality (ax-ext 2705) restated so that it postulates the existence of a set 𝑧 given two arbitrary sets 𝑥 and 𝑦. This way to express it follows the general idea of the other ZFC axioms, which is to postulate the existence of sets given other sets. (Contributed by NM, 28-Sep-2003.)
⊢ ∃𝑧((𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
Theorem	axextg 2707*	A generalization of the axiom of extensionality in which 𝑥 and 𝑦 need not be distinct. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) Remove dependencies on ax-10 2146, ax-12 2182, ax-13 2374. (Revised by BJ, 12-Jul-2019.) (Revised by Wolf Lammen, 9-Dec-2019.)
⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
Theorem	axextb 2708*	A bidirectional version of the axiom of extensionality. Although this theorem looks like a definition of equality, it requires the axiom of extensionality for its proof under our axiomatization. See the comments for ax-ext 2705 and df-cleq 2725. (Contributed by NM, 14-Nov-2008.)
⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
Theorem	axextmo 2709*	There exists at most one set with prescribed elements. Theorem 1.1 of [BellMachover] p. 462. (Contributed by NM, 30-Jun-1994.) (Proof shortened by Wolf Lammen, 13-Nov-2019.) Use the at-most-one quantifier. (Revised by BJ, 17-Sep-2022.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ∃*𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)
Theorem	nulmo 2710*	There exists at most one empty set. With either axnul 5247 or axnulALT 5246 or ax-nul 5248, this proves that there exists a unique empty set. In practice, once the language of classes is available, we use the stronger characterization among classes eq0 4301. (Contributed by NM, 22-Dec-2007.) Use the at-most-one quantifier. (Revised by BJ, 17-Sep-2022.) (Proof shortened by Wolf Lammen, 26-Apr-2023.)
⊢ ∃*𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2.1.2  Classes
2.1.2.1  Class abstractions
Syntax	cab 2711	Introduce the class abstraction (or class builder) notation: {𝑥 ∣ 𝜑} is the class of sets 𝑥 such that 𝜑(𝑥) is true. A setvar variable can be expressed as a class abstraction per Theorem cvjust 2727, justifying the substitution of class variables for setvar variables via the use of cv 1540.
class {𝑥 ∣ 𝜑}
Definition	df-clab 2712	Define class abstractions, that is, classes of the form {𝑦 ∣ 𝜑}, which is read "the class of sets 𝑦 such that 𝜑(𝑦)". A few remarks are in order: 1. The axiomatic statement df-clab 2712 does not define the class abstraction {𝑦 ∣ 𝜑} itself, that is, it does not have the form ⊢ {𝑦 ∣ 𝜑} = ... that a standard definition should have (for a good reason: equality itself has not yet been defined or axiomatized for class abstractions; it is defined later in df-cleq 2725). Instead, df-clab 2712 has the form ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ ...), meaning that it only defines what it means for a setvar to be a member of a class abstraction. As a consequence, one can say that df-clab 2712 defines class abstractions if and only if a class abstraction is completely determined by which elements belong to it, which is the content of the axiom of extensionality ax-ext 2705. Therefore, df-clab 2712 can be considered a definition only in systems that can prove ax-ext 2705 (and the necessary first-order logic). 2. As in all definitions, the definiendum (the left-hand side of the biconditional) has no disjoint variable conditions. In particular, the setvar variables 𝑥 and 𝑦 need not be distinct, and the formula 𝜑 may depend on both 𝑥 and 𝑦. This is necessary, as with all definitions, since if there was for instance a disjoint variable condition on 𝑥, 𝑦, then one could not do anything with expressions like 𝑥 ∈ {𝑥 ∣ 𝜑} which are sometimes useful to shorten proofs (because of abid 2715). Most often, however, 𝑥 does not occur in {𝑦 ∣ 𝜑} and 𝑦 is free in 𝜑. 3. Remark 1 stresses that df-clab 2712 does not have the standard form of a definition for a class, but one could be led to think it has the standard form of a definition for a formula. However, it also fails that test since the membership predicate ∈ has already appeared earlier (outside of syntax e.g. in ax-8 2115). Indeed, the definiendum extends, or "overloads", the membership predicate ∈ from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This is possible because of wcel 2113 and cab 2711, and it can be called an "extension" of the membership predicate because of wel 2114, whose proof uses cv 1540. An a posteriori justification for cv 1540 is given by cvjust 2727, stating that every setvar can be written as a class abstraction (though conversely not every class abstraction is a set, as illustrated by Russell's paradox ru 3736). 4. Proof techniques. Because class variables can be substituted with compound expressions and setvar variables cannot, it is often useful to convert a theorem containing a free setvar variable to a more general version with a class variable. This is done with theorems such as vtoclg 3509 which is used, for example, to convert elirrv 9493 to elirr 9495. 5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2712, df-cleq 2725, and df-clel 2808, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 30391), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2725 and df-clel 2808). One could be less strict and decide to call "definition" every axiomatic statement which provides an eliminable and conservative extension of the considered axiom system. But the notion of conservativity may be given two different meanings in set.mm, due to the difference between the "scheme level" of set.mm and the "object level" of classical treatments. For a proof that these three axiomatic statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ax-ext 2705, see Appendix of [Levy] p. 357. 6. References and history. The concept of class abstraction dates back to at least Frege, and is used by Whitehead and Russell. This definition is Definition 2.1 of [Quine] p. 16 and Axiom 4.3.1 of [Levy] p. 12. It is called the "axiom of class comprehension" by [Levy] p. 358, who treats the theory of classes as an extralogical extension to predicate logic and set theory axioms. He calls the construction {𝑦 ∣ 𝜑} a "class term". For a full description of how classes are introduced and how to recover the primitive language, see the books of Quine and Levy (and the comment of eqabb 2872 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2872. (Contributed by NM, 26-May-1993.) (Revised by BJ, 19-Aug-2023.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
Theorem	eleq1ab 2713	Extension (in the sense of Remark 3 of the comment of df-clab 2712) of elequ1 2120 from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This extension does not require ax-8 2115 contrary to elequ1 2120, but recall from Remark 3 of the comment of df-clab 2712 that it can be considered an extension only because of cvjust 2727, which does require ax-8 2115. This is an instance of eleq1w 2816 where the containing class is a class abstraction, and contrary to it, it can be proved without df-clel 2808. See also eleq1 2821 for general classes. The straightforward yet important fact that this statement can be proved from FOL= plus df-clab 2712 (hence without ax-ext 2705, df-cleq 2725 or df-clel 2808) was stressed by Mario Carneiro. (Contributed by BJ, 17-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑧 ∣ 𝜑} ↔ 𝑦 ∈ {𝑧 ∣ 𝜑}))
Theorem	cleljustab 2714*	Extension of cleljust 2122 from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This is an instance of dfclel 2809 where the containing class is a class abstraction. The same remarks as for eleq1ab 2713 apply. (Contributed by BJ, 8-Nov-2021.) (Proof shortened by Steven Nguyen, 19-May-2023.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ {𝑦 ∣ 𝜑}))
Theorem	abid 2715	Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993.)
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
Theorem	vexwt 2716	A standard theorem of predicate calculus (stdpc4 2073) expressed using class abstractions. Closed form of vexw 2717. (Contributed by BJ, 14-Jun-2019.)
⊢ (∀𝑥𝜑 → 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	vexw 2717	If 𝜑 is a theorem, then any set belongs to the class {𝑥 ∣ 𝜑}. Therefore, {𝑥 ∣ 𝜑} is "a" universal class. This is the closest one can get to defining a universal class, or proving vex 3442, without using ax-ext 2705. Note that this theorem has no disjoint variable condition and does not use df-clel 2808 nor df-cleq 2725 either: only propositional logic and ax-gen 1796 and df-clab 2712. This is sbt 2071 expressed using class abstractions. Without ax-ext 2705, one cannot define "the" universal class, since one could not prove for instance the justification theorem {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} (see vjust 3439). Indeed, in order to prove any equality of classes, one needs df-cleq 2725, which has ax-ext 2705 as a hypothesis. Therefore, the classes {𝑥 ∣ ⊤}, {𝑦 ∣ (𝜑 → 𝜑)}, {𝑧 ∣ (∀𝑡𝑡 = 𝑡 → ∀𝑡𝑡 = 𝑡)} and countless others are all universal classes whose equality cannot be proved without ax-ext 2705. Once dfcleq 2726 is available, we will define "the" universal class in df-v 3440. Its degenerate instance is also a simple consequence of abid 2715 (using mpbir 231). (Contributed by BJ, 13-Jun-2019.) Reduce axiom dependencies. (Revised by Steven Nguyen, 25-Apr-2023.)
⊢ 𝜑    ⇒   ⊢ 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	vextru 2718	Every setvar is a member of {𝑥 ∣ ⊤}, which is therefore "a" universal class. Once class extensionality dfcleq 2726 is available, we can say "the" universal class (see df-v 3440). This is sbtru 2072 expressed using class abstractions. (Contributed by BJ, 2-Sep-2023.)
⊢ 𝑦 ∈ {𝑥 ∣ ⊤}
Theorem	nfsab1 2719*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove use of ax-12 2182. (Revised by SN, 20-Sep-2023.)
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	hbab1 2720*	Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2024.)
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → ∀𝑥 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	hbab 2721*	Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 1-Mar-1995.) Add disjoint variable condition to avoid ax-13 2374. See hbabg 2722 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} → ∀𝑥 𝑧 ∈ {𝑦 ∣ 𝜑})
Theorem	hbabg 2722*	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2374. See hbab 2721 for a version with more disjoint variable conditions, but not requiring ax-13 2374. (Contributed by NM, 1-Mar-1995.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} → ∀𝑥 𝑧 ∈ {𝑦 ∣ 𝜑})
Theorem	nfsab 2723*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2374. See nfsabg 2724 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
Theorem	nfsabg 2724*	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2374. See nfsab 2723 for a version with more disjoint variable conditions, but not requiring ax-13 2374. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
2.1.2.2  Class equality This section introduces class equality in df-cleq 2725. Note that apart from the local introduction of class variables to state the syntax axioms wceq 1541 and wcel 2113, this section is the first to use class variables. Therefore, the file set.mm contains declarations of class variables at the beginning of this section (not visible on the webpages).
Definition	df-cleq 2725*	Define the equality connective between classes. Definition 2.7 of [Quine] p. 18. Also Definition 4.5 of [TakeutiZaring] p. 13; Chapter 4 provides its justification and methods for eliminating it. Note that its elimination will not necessarily result in a single wff in the original language but possibly a "scheme" of wffs. The hypotheses express that all instances of the conclusion where class variables are replaced with setvar variables hold. Therefore, this definition merely extends to class variables something that is true for setvar variables, hence is conservative. This is only a proof sketch of conservativity; for details see Appendix of [Levy] p. 357. This is the reason why we call this axiomatic statement a "definition", even though it does not have the usual form of a definition. If we required a definition to have the usual form, we would call df-cleq 2725 an axiom. See also comments under df-clab 2712, df-clel 2808, and eqabb 2872. In the form of dfcleq 2726, this is called the "axiom of extensionality" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. While the three class definitions df-clab 2712, df-cleq 2725, and df-clel 2808 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 2808. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.)
⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))    &   ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	dfcleq 2726*	The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2705) and the definition of class equality (df-cleq 2725). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2708 to prove also the hypothesis of df-cleq 2725 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1796, equid 2013 }. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.)
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	cvjust 2727*	Every set is a class. Proposition 4.9 of [TakeutiZaring] p. 13. This theorem shows that a setvar variable can be expressed as a class abstraction. This provides a motivation for the class syntax construction cv 1540, which allows to substitute a setvar variable for a class variable. See also cab 2711 and df-clab 2712. Note that this is not a rigorous justification, because cv 1540 is used as part of the proof of this theorem, but a careful argument can be made outside of the formalism of Metamath, for example as is done in Chapter 4 of Takeuti and Zaring. See also the discussion under the definition of class in [Jech] p. 4 showing that "Every set can be considered to be a class." See abid1 2869 for the version of cvjust 2727 extended to classes. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2374. (Revised by Wolf Lammen, 4-May-2023.)
⊢ 𝑥 = {𝑦 ∣ 𝑦 ∈ 𝑥}
Theorem	ax9ALT 2728	Proof of ax-9 2123 from Tarski's FOL and dfcleq 2726. For a version not using ax-8 2115 either, see eleq2w2 2729. This shows that dfcleq 2726 is too powerful to be used as a definition instead of df-cleq 2725. Note that ax-ext 2705 is also a direct consequence of dfcleq 2726 (as an instance of its forward implication). (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
Theorem	eleq2w2 2729*	A weaker version of eleq2 2822 (but stronger than ax-9 2123 and elequ2 2128) that uses ax-12 2182 to avoid ax-8 2115 and df-clel 2808. Compare eleq2w 2817, whose setvars appear where the class variables are in this theorem, and vice versa. (Contributed by BJ, 24-Jun-2019.) Strengthen from setvar variables to class variables. (Revised by WL and SN, 23-Aug-2024.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	eqriv 2730*	Infer equality of classes from equivalence of membership. (Contributed by NM, 21-Jun-1993.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)    ⇒   ⊢ 𝐴 = 𝐵
Theorem	eqrdv 2731*	Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqrdav 2732*	Deduce equality of classes from an equivalence of membership that depends on the membership variable. (Contributed by NM, 7-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqid 2733	Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine] p. 41. This is part of Frege's eighth axiom per Proposition 54 of [Frege1879] p. 50; see also biid 261. An early mention of this law can be found in Aristotle, Metaphysics, Z.17, 1041a10-20. (Thanks to Stefan Allan and BJ for this information.) (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 14-Oct-2017.)
⊢ 𝐴 = 𝐴
Theorem	eqidd 2734	Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
⊢ (𝜑 → 𝐴 = 𝐴)
Theorem	eqeq1d 2735	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq1dALT 2736	Alternate proof of eqeq1d 2735, shorter but requiring ax-12 2182. (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen, 19-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq1 2737	Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq1i 2738	Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
Theorem	eqcomd 2739	Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.) Allow shortening of eqcom 2740. (Revised by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐴)
Theorem	eqcom 2740	Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
Theorem	eqcoms 2741	Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 24-Jun-1993.)
⊢ (𝐴 = 𝐵 → 𝜑)    ⇒   ⊢ (𝐵 = 𝐴 → 𝜑)
Theorem	eqcomi 2742	Inference from commutative law for class equality. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 = 𝐴
Theorem	neqcomd 2743	Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐵 = 𝐴)
Theorem	eqeq2d 2744	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) Allow shortening of eqeq2 2745. (Revised by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
Theorem	eqeq2 2745	Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
Theorem	eqeq2i 2746	Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)
Theorem	eqeqan12d 2747	A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2752. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) Shorten other proofs. (Revised by Wolf Lammen, 23-Oct-2024.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeqan12rd 2748	A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeq12d 2749	A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Oct-2024.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeq12 2750	Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeq12i 2751	A useful inference for substituting definitions into an equality. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)
Theorem	eqeqan12dALT 2752	Alternate proof of eqeqan12d 2747. This proof has one more step but one fewer essential step. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqtr 2753	Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
Theorem	eqtr2 2754	A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 24-Oct-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)
Theorem	eqtr3 2755	A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Wolf Lammen, 24-Oct-2024.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
Theorem	eqtri 2756	An equality transitivity inference. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 = 𝐶
Theorem	eqtr2i 2757	An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐶 = 𝐴
Theorem	eqtr3i 2758	An equality transitivity inference. (Contributed by NM, 6-May-1994.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    ⇒   ⊢ 𝐵 = 𝐶
Theorem	eqtr4i 2759	An equality transitivity inference. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 = 𝐶
Theorem	3eqtri 2760	An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐴 = 𝐷
Theorem	3eqtrri 2761	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐷 = 𝐴
Theorem	3eqtr2i 2762	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐴 = 𝐷
Theorem	3eqtr2ri 2763	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐷 = 𝐴
Theorem	3eqtr3i 2764	An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐶 = 𝐷
Theorem	3eqtr3ri 2765	An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐷 = 𝐶
Theorem	3eqtr4i 2766	An inference from three chained equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐶 = 𝐷
Theorem	3eqtr4ri 2767	An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐷 = 𝐶
Theorem	eqtrd 2768	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2d 2769	An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr3d 2770	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	eqtr4d 2771	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	3eqtrd 2772	A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐷)
Theorem	3eqtrrd 2773	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐴)
Theorem	3eqtr2d 2774	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐷)
Theorem	3eqtr2rd 2775	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐴)
Theorem	3eqtr3d 2776	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr3rd 2777	A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	3eqtr4d 2778	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4rd 2779	A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	eqtrid 2780	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2id 2781	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr3id 2782	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr3di 2783	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐴 = 𝐶    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	eqtrdi 2784	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2di 2785	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr4di 2786	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr4id 2787	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	sylan9eq 2788	An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
Theorem	sylan9req 2789	An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
Theorem	sylan9eqr 2790	An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)
Theorem	3eqtr3g 2791	A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr3a 2792	A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4g 2793	A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4a 2794	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 2795	A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
⊢ (𝐴 = 𝐶 → 𝐷 = 𝐹)    &   ⊢ (𝐵 = 𝐷 → 𝐶 = 𝐺)    ⇒   ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐹) ↔ (𝐵 = 𝐷 ∧ 𝐴 = 𝐺))
Theorem	iseqsetvlem 2796*	Lemma for iseqsetv-cleq 2797. (Contributed by Wolf Lammen, 17-Aug-2025.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑧 𝑧 = 𝐴)
Theorem	iseqsetv-cleq 2797*	Alternate proof of iseqsetv-clel 2812. The expression ∃𝑥𝑥 = 𝐴 does not depend on a particular choice of the set variable. The proof here avoids df-clab 2712, df-clel 2808 and ax-8 2115, but instead is based on ax-9 2123, ax-ext 2705 and df-cleq 2725. 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 2712, or you need df-cleq 2725 anyway. See the alternative version , not using df-cleq 2725 or ax-ext 2705 or ax-9 2123. (Contributed by Wolf Lammen, 6-Aug-2025.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	abbi 2798	Equivalent formulas yield equal class abstractions (closed form). This is the backward implication of abbib 2802, proved from fewer axioms, and hence is independently named. (Contributed by BJ and WL and SN, 20-Aug-2023.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
Theorem	abbidv 2799*	Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2182, based on an idea of Steven Nguyen. (Revised by Wolf Lammen, 6-May-2023.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	abbii 2800	Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2146, ax-11 2162, and ax-12 2182. (Revised by Steven Nguyen, 3-May-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}