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	axio 2701	Definition of 'or' (intuitionistic logic axiom ax-io). (Contributed by Jim Kingdon, 21-May-2018.) (New usage is discouraged.)
⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓)))
Theorem	axi4 2702	Specialization (intuitionistic logic axiom ax-4). This is just sp 2180 by another name. (Contributed by Jim Kingdon, 31-Dec-2017.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axi5r 2703	Converse of axc4 2319 (intuitionistic logic axiom ax-i5r). (Contributed by Jim Kingdon, 31-Dec-2017.)
⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑 → 𝜓))
Theorem	axial 2704	The setvar 𝑥 is not free in ∀𝑥𝜑 (intuitionistic logic axiom ax-ial). (Contributed by Jim Kingdon, 31-Dec-2017.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	axie1 2705	The setvar 𝑥 is not free in ∃𝑥𝜑 (intuitionistic logic axiom ax-ie1). (Contributed by Jim Kingdon, 31-Dec-2017.) (New usage is discouraged.)
⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
Theorem	axie2 2706	A key property of existential quantification (intuitionistic logic axiom ax-ie2). (Contributed by Jim Kingdon, 31-Dec-2017.)
⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
Theorem	axi9 2707	Axiom of existence (intuitionistic logic axiom ax-i9). In classical logic, this is equivalent to ax-6 1975 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 2708	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 2709	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 2158. (Revised by Wolf Lammen, 24-Apr-2023.) (New usage is discouraged.)
⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Theorem	axbnd 2710	Axiom of Bundling (intuitionistic logic axiom ax-bnd). In classical logic, this and axi12 2709 are fairly straightforward consequences of axc9 2384. But in intuitionistic logic, it is not easy to add the extra ∀𝑥 to axi12 2709 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 3719), 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 2712.) 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 2711*	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 2126. 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 2711 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 5214, 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 2711 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 2712*	The axiom of extensionality (ax-ext 2711) 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 2713*	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 2141, ax-12 2175, ax-13 2374. (Revised by BJ, 12-Jul-2019.) (Revised by Wolf Lammen, 9-Dec-2019.)
⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
Theorem	axextb 2714*	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 2711 and df-cleq 2732. (Contributed by NM, 14-Nov-2008.)
⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
Theorem	axextmo 2715*	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 2716*	There exists at most one empty set. With either axnul 5233 or axnulALT 5232 or ax-nul 5234, 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 4283. (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 2717	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 2734, justifying the substitution of class variables for setvar variables via the use of cv 1541.
class {𝑥 ∣ 𝜑}
Definition	df-clab 2718	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 2718 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 2732). Instead, df-clab 2718 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 2718 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 2711. Therefore, df-clab 2718 can be considered a definition only in systems that can prove ax-ext 2711 (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 2721). Most often, however, 𝑥 does not occur in {𝑦 ∣ 𝜑} and 𝑦 is free in 𝜑. 3. Remark 1 stresses that df-clab 2718 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 2112). 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 2110 and cab 2717, and it can be called an "extension" of the membership predicate because of wel 2111, whose proof uses cv 1541. An a posteriori justification for cv 1541 is given by cvjust 2734, 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 3719). 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 3504 which is used, for example, to convert elirrv 9333 to elirr 9334. 5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2718, df-cleq 2732, and df-clel 2818, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 28760), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2732 and df-clel 2818). 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 2711, 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 abeq2 2874 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2874. (Contributed by NM, 26-May-1993.) (Revised by BJ, 19-Aug-2023.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
Theorem	eleq1ab 2719	Extension (in the sense of Remark 3 of the comment of df-clab 2718) of elequ1 2117 from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This extension does not require ax-8 2112 contrary to elequ1 2117, but recall from Remark 3 of the comment of df-clab 2718 that it can be considered an extension only because of cvjust 2734, which does require ax-8 2112. This is an instance of eleq1w 2823 where the containing class is a class abstraction, and contrary to it, it can be proved without df-clel 2818. See also eleq1 2828 for general classes. The straightforward yet important fact that this statement can be proved from FOL= plus df-clab 2718 (hence without ax-ext 2711, df-cleq 2732 or df-clel 2818) was stressed by Mario Carneiro. (Contributed by BJ, 17-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑧 ∣ 𝜑} ↔ 𝑦 ∈ {𝑧 ∣ 𝜑}))
Theorem	cleljustab 2720*	Extension of cleljust 2119 from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This is an instance of dfclel 2819 where the containing class is a class abstraction. The same remarks as for eleq1ab 2719 apply. (Contributed by BJ, 8-Nov-2021.) (Proof shortened by Steven Nguyen, 19-May-2023.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ {𝑦 ∣ 𝜑}))
Theorem	abid 2721	Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993.)
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
Theorem	vexwt 2722	A standard theorem of predicate calculus (stdpc4 2075) expressed using class abstractions. Closed form of vexw 2723. (Contributed by BJ, 14-Jun-2019.)
⊢ (∀𝑥𝜑 → 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	vexw 2723	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 3435, without using ax-ext 2711. Note that this theorem has no disjoint variable condition and does not use df-clel 2818 nor df-cleq 2732 either: only propositional logic and ax-gen 1802 and df-clab 2718. This is sbt 2073 expressed using class abstractions. Without ax-ext 2711, one cannot define "the" universal class, since one could not prove for instance the justification theorem {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} (see vjust 3432). Indeed, in order to prove any equality of classes, one needs df-cleq 2732, which has ax-ext 2711 as a hypothesis. Therefore, the classes {𝑥 ∣ ⊤}, {𝑦 ∣ (𝜑 → 𝜑)}, {𝑧 ∣ (∀𝑡𝑡 = 𝑡 → ∀𝑡𝑡 = 𝑡)} and countless others are all universal classes whose equality cannot be proved without ax-ext 2711. Once dfcleq 2733 is available, we will define "the" universal class in df-v 3433. Its degenerate instance is also a simple consequence of abid 2721 (using mpbir 230). (Contributed by BJ, 13-Jun-2019.) Reduce axiom dependencies. (Revised by Steven Nguyen, 25-Apr-2023.)
⊢ 𝜑    ⇒   ⊢ 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	vextru 2724	Every setvar is a member of {𝑥 ∣ ⊤}, which is therefore "a" universal class. Once class extensionality dfcleq 2733 is available, we can say "the" universal class (see df-v 3433). This is sbtru 2074 expressed using class abstractions. (Contributed by BJ, 2-Sep-2023.)
⊢ 𝑦 ∈ {𝑥 ∣ ⊤}
Theorem	nfsab1 2725*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove use of ax-12 2175. (Revised by SN, 20-Sep-2023.)
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	hbab1 2726*	Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2024.)
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → ∀𝑥 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	hbab1OLD 2727*	Obsolete version of hbab1 2726 as of 25-Oct-2024. (Contributed by NM, 26-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → ∀𝑥 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	hbab 2728*	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 2729 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} → ∀𝑥 𝑧 ∈ {𝑦 ∣ 𝜑})
Theorem	hbabg 2729*	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2374. See hbab 2728 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 2730*	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 2731 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
Theorem	nfsabg 2731*	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2374. See nfsab 2730 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 2732. Note that apart from the local introduction of class variables to state the syntax axioms wceq 1542 and wcel 2110, 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 2732*	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 2732 an axiom. See also comments under df-clab 2718, df-clel 2818, and abeq2 2874. In the form of dfcleq 2733, 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 2718, df-cleq 2732, and df-clel 2818 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 2818. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.)
⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))    &   ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	dfcleq 2733*	The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2711) and the definition of class equality (df-cleq 2732). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2714 to prove also the hypothesis of df-cleq 2732 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1802, equid 2019 }. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.)
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	cvjust 2734*	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 1541, which allows us to substitute a setvar variable for a class variable. See also cab 2717 and df-clab 2718. Note that this is not a rigorous justification, because cv 1541 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 2883 for the version of cvjust 2734 extended to classes. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2374. (Revised by Wolf Lammen, 4-May-2023.)
⊢ 𝑥 = {𝑦 ∣ 𝑦 ∈ 𝑥}
Theorem	ax9ALT 2735	Proof of ax-9 2120 from Tarski's FOL and dfcleq 2733. For a version not using ax-8 2112 either, see eleq2w2 2736. This shows that dfcleq 2733 is too powerful to be used as a definition instead of df-cleq 2732. Note that ax-ext 2711 is also a direct consequence of dfcleq 2733 (as an instance of its forward implication). (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
Theorem	eleq2w2 2736*	A weaker version of eleq2 2829 (but stronger than ax-9 2120 and elequ2 2125) that uses ax-12 2175 to avoid ax-8 2112 and df-clel 2818. Compare eleq2w 2824, 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 2737*	Infer equality of classes from equivalence of membership. (Contributed by NM, 21-Jun-1993.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)    ⇒   ⊢ 𝐴 = 𝐵
Theorem	eqrdv 2738*	Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqrdav 2739*	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 2740	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 2741	Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
⊢ (𝜑 → 𝐴 = 𝐴)
Theorem	eqeq1d 2742	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 2743	Alternate proof of eqeq1d 2742, shorter but requiring ax-12 2175. (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen, 19-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq1 2744	Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq1i 2745	Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
Theorem	eqcomd 2746	Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.) Allow shortening of eqcom 2747. (Revised by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐴)
Theorem	eqcom 2747	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 2748	Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 24-Jun-1993.)
⊢ (𝐴 = 𝐵 → 𝜑)    ⇒   ⊢ (𝐵 = 𝐴 → 𝜑)
Theorem	eqcomi 2749	Inference from commutative law for class equality. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 = 𝐴
Theorem	neqcomd 2750	Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐵 = 𝐴)
Theorem	eqeq2d 2751	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) Allow shortening of eqeq2 2752. (Revised by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
Theorem	eqeq2 2752	Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
Theorem	eqeq2i 2753	Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)
Theorem	eqeqan12d 2754	A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2762. (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 2755	A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeq12d 2756	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 2757	Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeq12i 2758	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 2759	Obsolete version of eqeq12 2757 as of 23-Oct-2024. (Contributed by NM, 3-Aug-1994.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeq12dOLD 2760	Obsolete version of eqeq12d 2756 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 2761	Obsolete version of eqeqan12d 2754 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 2762	Alternate proof of eqeqan12d 2754. 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 2763	Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
Theorem	eqtr2 2764	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 2765	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 2766	A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Wolf Lammen, 24-Oct-2024.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
Theorem	eqtr3OLD 2767	Obsolete version of eqtr3 2766 as of 24-Oct-2024. (Contributed by NM, 20-May-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
Theorem	eqtri 2768	An equality transitivity inference. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 = 𝐶
Theorem	eqtr2i 2769	An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐶 = 𝐴
Theorem	eqtr3i 2770	An equality transitivity inference. (Contributed by NM, 6-May-1994.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    ⇒   ⊢ 𝐵 = 𝐶
Theorem	eqtr4i 2771	An equality transitivity inference. (Contributed by NM, 26-May-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 = 𝐶
Theorem	3eqtri 2772	An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐴 = 𝐷
Theorem	3eqtrri 2773	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐷 = 𝐴
Theorem	3eqtr2i 2774	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐴 = 𝐷
Theorem	3eqtr2ri 2775	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐷 = 𝐴
Theorem	3eqtr3i 2776	An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐶 = 𝐷
Theorem	3eqtr3ri 2777	An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐷 = 𝐶
Theorem	3eqtr4i 2778	An inference from three chained equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐶 = 𝐷
Theorem	3eqtr4ri 2779	An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐷 = 𝐶
Theorem	eqtrd 2780	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2d 2781	An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr3d 2782	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	eqtr4d 2783	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	3eqtrd 2784	A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐷)
Theorem	3eqtrrd 2785	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐴)
Theorem	3eqtr2d 2786	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐷)
Theorem	3eqtr2rd 2787	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐴)
Theorem	3eqtr3d 2788	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr3rd 2789	A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	3eqtr4d 2790	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4rd 2791	A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	eqtrid 2792	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2id 2793	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr3id 2794	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr3di 2795	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐴 = 𝐶    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	eqtrdi 2796	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2di 2797	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr4di 2798	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr4id 2799	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	sylan9eq 2800	An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)