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	axi12 2701	Axiom of Quantifier Introduction (intuitionistic logic axiom ax-i12). In classical logic, this is mostly a restatement of axc9 2381 (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 2371. (Contributed by Jim Kingdon, 31-Dec-2017.) Avoid ax-11 2154. (Revised by Wolf Lammen, 24-Apr-2023.) (New usage is discouraged.)
⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Theorem	axbnd 2702	Axiom of Bundling (intuitionistic logic axiom ax-bnd). In classical logic, this and axi12 2701 are fairly straightforward consequences of axc9 2381. But in intuitionistic logic, it is not easy to add the extra ∀𝑥 to axi12 2701 and so we treat the two as separate axioms. Usage of this theorem is discouraged because it depends on ax-13 2371. (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 3776), 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 2704.) 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 2703*	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 2122. 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 2703 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 5285, 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 2703 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 2704*	The axiom of extensionality (ax-ext 2703) 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 2705*	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 2137, ax-12 2171, ax-13 2371. (Revised by BJ, 12-Jul-2019.) (Revised by Wolf Lammen, 9-Dec-2019.)
⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
Theorem	axextb 2706*	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 2703 and df-cleq 2724. (Contributed by NM, 14-Nov-2008.)
⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
Theorem	axextmo 2707*	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 2708*	There exists at most one empty set. With either axnul 5305 or axnulALT 5304 or ax-nul 5306, 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 4343. (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 2709	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 2726, justifying the substitution of class variables for setvar variables via the use of cv 1540.
class {𝑥 ∣ 𝜑}
Definition	df-clab 2710	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 2710 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 2724). Instead, df-clab 2710 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 2710 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 2703. Therefore, df-clab 2710 can be considered a definition only in systems that can prove ax-ext 2703 (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 2713). Most often, however, 𝑥 does not occur in {𝑦 ∣ 𝜑} and 𝑦 is free in 𝜑. 3. Remark 1 stresses that df-clab 2710 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 (e.g., in the non-syntactic statement ax-8 2108). 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 2106 and cab 2709, and it can be called an "extension" of the membership predicate because of wel 2107, whose proof uses cv 1540. An a posteriori justification for cv 1540 is given by cvjust 2726, 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 3776). 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 3556 which is used, for example, to convert elirrv 9593 to elirr 9594. 5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2710, df-cleq 2724, and df-clel 2810, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 29691), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2724 and df-clel 2810). 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 2703, 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 2873 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2873. (Contributed by NM, 26-May-1993.) (Revised by BJ, 19-Aug-2023.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
Theorem	eleq1ab 2711	Extension (in the sense of Remark 3 of the comment of df-clab 2710) of elequ1 2113 from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This extension does not require ax-8 2108 contrary to elequ1 2113, but recall from Remark 3 of the comment of df-clab 2710 that it can be considered an extension only because of cvjust 2726, which does require ax-8 2108. 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 2810. See also eleq1 2821 for general classes. The straightforward yet important fact that this statement can be proved from FOL= plus df-clab 2710 (hence without ax-ext 2703, df-cleq 2724 or df-clel 2810) was stressed by Mario Carneiro. (Contributed by BJ, 17-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑧 ∣ 𝜑} ↔ 𝑦 ∈ {𝑧 ∣ 𝜑}))
Theorem	cleljustab 2712*	Extension of cleljust 2115 from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This is an instance of dfclel 2811 where the containing class is a class abstraction. The same remarks as for eleq1ab 2711 apply. (Contributed by BJ, 8-Nov-2021.) (Proof shortened by Steven Nguyen, 19-May-2023.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ {𝑦 ∣ 𝜑}))
Theorem	abid 2713	Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993.)
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
Theorem	vexwt 2714	A standard theorem of predicate calculus (stdpc4 2071) expressed using class abstractions. Closed form of vexw 2715. (Contributed by BJ, 14-Jun-2019.)
⊢ (∀𝑥𝜑 → 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	vexw 2715	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 3478, without using ax-ext 2703. Note that this theorem has no disjoint variable condition and does not use df-clel 2810 nor df-cleq 2724 either: only propositional logic and ax-gen 1797 and df-clab 2710. This is sbt 2069 expressed using class abstractions. Without ax-ext 2703, one cannot define "the" universal class, since one could not prove for instance the justification theorem {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} (see vjust 3475). Indeed, in order to prove any equality of classes, one needs df-cleq 2724, which has ax-ext 2703 as a hypothesis. Therefore, the classes {𝑥 ∣ ⊤}, {𝑦 ∣ (𝜑 → 𝜑)}, {𝑧 ∣ (∀𝑡𝑡 = 𝑡 → ∀𝑡𝑡 = 𝑡)} and countless others are all universal classes whose equality cannot be proved without ax-ext 2703. Once dfcleq 2725 is available, we will define "the" universal class in df-v 3476. Its degenerate instance is also a simple consequence of abid 2713 (using mpbir 230). (Contributed by BJ, 13-Jun-2019.) Reduce axiom dependencies. (Revised by Steven Nguyen, 25-Apr-2023.)
⊢ 𝜑    ⇒   ⊢ 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	vextru 2716	Every setvar is a member of {𝑥 ∣ ⊤}, which is therefore "a" universal class. Once class extensionality dfcleq 2725 is available, we can say "the" universal class (see df-v 3476). This is sbtru 2070 expressed using class abstractions. (Contributed by BJ, 2-Sep-2023.)
⊢ 𝑦 ∈ {𝑥 ∣ ⊤}
Theorem	nfsab1 2717*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove use of ax-12 2171. (Revised by SN, 20-Sep-2023.)
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	hbab1 2718*	Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2024.)
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → ∀𝑥 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	hbab1OLD 2719*	Obsolete version of hbab1 2718 as of 25-Oct-2024. (Contributed by NM, 26-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → ∀𝑥 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	hbab 2720*	Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 1-Mar-1995.) Add disjoint variable condition to avoid ax-13 2371. See hbabg 2721 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} → ∀𝑥 𝑧 ∈ {𝑦 ∣ 𝜑})
Theorem	hbabg 2721*	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2371. See hbab 2720 for a version with more disjoint variable conditions, but not requiring ax-13 2371. (Contributed by NM, 1-Mar-1995.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} → ∀𝑥 𝑧 ∈ {𝑦 ∣ 𝜑})
Theorem	nfsab 2722*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2371. See nfsabg 2723 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
Theorem	nfsabg 2723*	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2371. See nfsab 2722 for a version with more disjoint variable conditions, but not requiring ax-13 2371. (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 2724. Note that apart from the local introduction of class variables to state the syntax axioms wceq 1541 and wcel 2106, 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 2724*	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 2724 an axiom. See also comments under df-clab 2710, df-clel 2810, and eqabb 2873. In the form of dfcleq 2725, 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 2710, df-cleq 2724, and df-clel 2810 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 2810. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.)
⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))    &   ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	dfcleq 2725*	The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2703) and the definition of class equality (df-cleq 2724). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2706 to prove also the hypothesis of df-cleq 2724 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1797, equid 2015 }. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.)
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	cvjust 2726*	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 2709 and df-clab 2710. 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 2870 for the version of cvjust 2726 extended to classes. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2371. (Revised by Wolf Lammen, 4-May-2023.)
⊢ 𝑥 = {𝑦 ∣ 𝑦 ∈ 𝑥}
Theorem	ax9ALT 2727	Proof of ax-9 2116 from Tarski's FOL and dfcleq 2725. For a version not using ax-8 2108 either, see eleq2w2 2728. This shows that dfcleq 2725 is too powerful to be used as a definition instead of df-cleq 2724. Note that ax-ext 2703 is also a direct consequence of dfcleq 2725 (as an instance of its forward implication). (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
Theorem	eleq2w2 2728*	A weaker version of eleq2 2822 (but stronger than ax-9 2116 and elequ2 2121) that uses ax-12 2171 to avoid ax-8 2108 and df-clel 2810. 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 2729*	Infer equality of classes from equivalence of membership. (Contributed by NM, 21-Jun-1993.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)    ⇒   ⊢ 𝐴 = 𝐵
Theorem	eqrdv 2730*	Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqrdav 2731*	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 2732	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 260. 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 2733	Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
⊢ (𝜑 → 𝐴 = 𝐴)
Theorem	eqeq1d 2734	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 2735	Alternate proof of eqeq1d 2734, shorter but requiring ax-12 2171. (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen, 19-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq1 2736	Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq1i 2737	Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
Theorem	eqcomd 2738	Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.) Allow shortening of eqcom 2739. (Revised by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐴)
Theorem	eqcom 2739	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 2740	Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 24-Jun-1993.)
⊢ (𝐴 = 𝐵 → 𝜑)    ⇒   ⊢ (𝐵 = 𝐴 → 𝜑)
Theorem	eqcomi 2741	Inference from commutative law for class equality. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 = 𝐴
Theorem	neqcomd 2742	Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐵 = 𝐴)
Theorem	eqeq2d 2743	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) Allow shortening of eqeq2 2744. (Revised by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
Theorem	eqeq2 2744	Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
Theorem	eqeq2i 2745	Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)
Theorem	eqeqan12d 2746	A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2754. (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 2747	A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeq12d 2748	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 2749	Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeq12i 2750	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	eqeq12OLD 2751	Obsolete version of eqeq12 2749 as of 23-Oct-2024. (Contributed by NM, 3-Aug-1994.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeq12dOLD 2752	Obsolete version of eqeq12d 2748 as of 23-Oct-2024. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeqan12dOLD 2753	Obsolete version of eqeqan12d 2746 as of 23-Oct-2024. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeqan12dALT 2754	Alternate proof of eqeqan12d 2746. 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 2755	Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
Theorem	eqtr2 2756	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	eqtr2OLD 2757	Obsolete version of eqtr2 as of 24-Oct-2024. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)
Theorem	eqtr3 2758	A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Wolf Lammen, 24-Oct-2024.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
Theorem	eqtr3OLD 2759	Obsolete version of eqtr3 2758 as of 24-Oct-2024. (Contributed by NM, 20-May-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
Theorem	eqtri 2760	An equality transitivity inference. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 = 𝐶
Theorem	eqtr2i 2761	An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐶 = 𝐴
Theorem	eqtr3i 2762	An equality transitivity inference. (Contributed by NM, 6-May-1994.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    ⇒   ⊢ 𝐵 = 𝐶
Theorem	eqtr4i 2763	An equality transitivity inference. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 = 𝐶
Theorem	3eqtri 2764	An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐴 = 𝐷
Theorem	3eqtrri 2765	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐷 = 𝐴
Theorem	3eqtr2i 2766	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐴 = 𝐷
Theorem	3eqtr2ri 2767	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐷 = 𝐴
Theorem	3eqtr3i 2768	An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐶 = 𝐷
Theorem	3eqtr3ri 2769	An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐷 = 𝐶
Theorem	3eqtr4i 2770	An inference from three chained equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐶 = 𝐷
Theorem	3eqtr4ri 2771	An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐷 = 𝐶
Theorem	eqtrd 2772	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2d 2773	An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr3d 2774	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	eqtr4d 2775	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	3eqtrd 2776	A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐷)
Theorem	3eqtrrd 2777	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐴)
Theorem	3eqtr2d 2778	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐷)
Theorem	3eqtr2rd 2779	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐴)
Theorem	3eqtr3d 2780	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr3rd 2781	A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	3eqtr4d 2782	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4rd 2783	A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	eqtrid 2784	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2id 2785	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr3id 2786	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr3di 2787	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐴 = 𝐶    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	eqtrdi 2788	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2di 2789	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr4di 2790	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr4id 2791	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	sylan9eq 2792	An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
Theorem	sylan9req 2793	An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
Theorem	sylan9eqr 2794	An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)
Theorem	3eqtr3g 2795	A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr3a 2796	A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4g 2797	A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4a 2798	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 2799	A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
⊢ (𝐴 = 𝐶 → 𝐷 = 𝐹)    &   ⊢ (𝐵 = 𝐷 → 𝐶 = 𝐺)    ⇒   ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐹) ↔ (𝐵 = 𝐷 ∧ 𝐴 = 𝐺))
Theorem	abbi 2800	Equivalent formulas yield equal class abstractions (closed form). This is the backward implication of abbib 2804, proved from fewer axioms, and hence is independently named. (Contributed by BJ and WL and SN, 20-Aug-2023.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})