P. 23 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2201-2300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfsab 2201*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
Definition	df-cleq 2202*	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. This is an example of a somewhat "risky" definition, meaning that it has a more complex than usual soundness justification (outside of Metamath), because it "overloads" or reuses the existing equality symbol rather than introducing a new symbol. This allows us to make statements that may not hold for the original symbol. For example, it permits us to deduce 𝑦 = 𝑧 ↔ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧), which is not a theorem of logic but rather presupposes the Axiom of Extensionality (see Theorem axext4 2193). We therefore include this axiom as a hypothesis, so that the use of Extensionality is properly indicated. We could avoid this complication by introducing a new symbol, say =2, in place of =. This would also have the advantage of making elimination of the definition straightforward, so that we could eliminate Extensionality as a hypothesis. We would then also have the advantage of being able to identify in various proofs exactly where Extensionality truly comes into play rather than just being an artifact of a definition. One of our theorems would then be 𝑥 =2 𝑦 ↔ 𝑥 = 𝑦 by invoking Extensionality. However, to conform to literature usage, we retain this overloaded definition. This also makes some proofs shorter and probably easier to read, without the constant switching between two kinds of equality. See also comments under df-clab 2196, df-clel 2205, and abeq2 2318. In the form of dfcleq 2203, 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. For a general discussion of the theory of classes, see https://us.metamath.org/mpeuni/mmset.html#class 2203. (Contributed by NM, 15-Sep-1993.)
⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	dfcleq 2203*	The same as df-cleq 2202 with the hypothesis removed using the Axiom of Extensionality ax-ext 2191. (Contributed by NM, 15-Sep-1993.)
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	cvjust 2204*	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 1374, which allows us to substitute a setvar variable for a class variable. See also cab 2195 and df-clab 2196. Note that this is not a rigorous justification, because cv 1374 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." (Contributed by NM, 7-Nov-2006.)
⊢ 𝑥 = {𝑦 ∣ 𝑦 ∈ 𝑥}
Definition	df-clel 2205*	Define the membership connective between classes. Theorem 6.3 of [Quine] p. 41, or Proposition 4.6 of [TakeutiZaring] p. 13, which we adopt as a definition. See these references for its metalogical justification. Note that like df-cleq 2202 it extends or "overloads" the use of the existing membership symbol, but unlike df-cleq 2202 it does not strengthen the set of valid wffs of logic when the class variables are replaced with setvar variables (see cleljust 2186), so we don't include any set theory axiom as a hypothesis. See also comments about the syntax under df-clab 2196. This is called the "axiom of membership" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. For a general discussion of the theory of classes, see https://us.metamath.org/mpeuni/mmset.html#class 2196. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	eqriv 2206*	Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)    ⇒   ⊢ 𝐴 = 𝐵
Theorem	eqrdv 2207*	Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqrdav 2208*	Deduce equality of classes from an equivalence of membership that depends on the membership variable. (Contributed by NM, 7-Nov-2008.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	eqid 2209	Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine] p. 41. This law is thought to have originated with Aristotle (Metaphysics, Zeta, 17, 1041 a, 10-20). (Thanks to Stefan Allan and BJ for this information.) (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 14-Oct-2017.)
⊢ 𝐴 = 𝐴
Theorem	eqidd 2210	Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
⊢ (𝜑 → 𝐴 = 𝐴)
Theorem	eqcom 2211	Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
Theorem	eqcoms 2212	Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → 𝜑)    ⇒   ⊢ (𝐵 = 𝐴 → 𝜑)
Theorem	eqcomi 2213	Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 = 𝐴
Theorem	neqcomd 2214	Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐵 = 𝐴)
Theorem	eqcomd 2215	Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐴)
Theorem	eqeq1 2216	Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq1i 2217	Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
Theorem	eqeq1d 2218	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
Theorem	eqeq2 2219	Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
Theorem	eqeq2i 2220	Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)
Theorem	eqeq2d 2221	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
Theorem	eqeq12 2222	Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeq12i 2223	A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)
Theorem	eqeq12d 2224	A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeqan12d 2225	A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqeqan12rd 2226	A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	eqtr 2227	Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
Theorem	eqtr2 2228	A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)
Theorem	eqtr3 2229	A transitive law for class equality. (Contributed by NM, 20-May-2005.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
Theorem	eqtri 2230	An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 = 𝐶
Theorem	eqtr2i 2231	An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐶 = 𝐴
Theorem	eqtr3i 2232	An equality transitivity inference. (Contributed by NM, 6-May-1994.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    ⇒   ⊢ 𝐵 = 𝐶
Theorem	eqtr4i 2233	An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 = 𝐶
Theorem	3eqtri 2234	An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐴 = 𝐷
Theorem	3eqtrri 2235	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐷 = 𝐴
Theorem	3eqtr2i 2236	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐴 = 𝐷
Theorem	3eqtr2ri 2237	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ 𝐷 = 𝐴
Theorem	3eqtr3i 2238	An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐶 = 𝐷
Theorem	3eqtr3ri 2239	An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐷 = 𝐶
Theorem	3eqtr4i 2240	An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐶 = 𝐷
Theorem	3eqtr4ri 2241	An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐷 = 𝐶
Theorem	eqtrd 2242	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2d 2243	An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr3d 2244	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	eqtr4d 2245	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	3eqtrd 2246	A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐷)
Theorem	3eqtrrd 2247	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐴)
Theorem	3eqtr2d 2248	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐷)
Theorem	3eqtr2rd 2249	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐴)
Theorem	3eqtr3d 2250	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr3rd 2251	A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	3eqtr4d 2252	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4rd 2253	A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐷 = 𝐶)
Theorem	eqtrid 2254	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2id 2255	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr3id 2256	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr3di 2257	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐴 = 𝐶    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	eqtrdi 2258	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr2di 2259	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐶 = 𝐴)
Theorem	eqtr4di 2260	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	eqtr4id 2261	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	sylan9eq 2262	An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
Theorem	sylan9req 2263	An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
Theorem	sylan9eqr 2264	An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)
Theorem	3eqtr3g 2265	A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr3a 2266	A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4g 2267	A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 = 𝐷)
Theorem	3eqtr4a 2268	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 2269	A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
⊢ (𝐴 = 𝐶 → 𝐷 = 𝐹)    &   ⊢ (𝐵 = 𝐷 → 𝐶 = 𝐺)    ⇒   ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐹) ↔ (𝐵 = 𝐷 ∧ 𝐴 = 𝐺))
Theorem	eleq1w 2270	Weaker version of eleq1 2272 (but more general than elequ1 2184) not depending on ax-ext 2191 nor df-cleq 2202. (Contributed by BJ, 24-Jun-2019.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
Theorem	eleq2w 2271	Weaker version of eleq2 2273 (but more general than elequ2 2185) not depending on ax-ext 2191 nor df-cleq 2202. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))
Theorem	eleq1 2272	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
Theorem	eleq2 2273	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
Theorem	eleq12 2274	Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))
Theorem	eleq1i 2275	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
Theorem	eleq2i 2276	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)
Theorem	eleq12i 2277	Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)
Theorem	eleq1d 2278	Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
Theorem	eleq2d 2279	Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
Theorem	eleq12d 2280	Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))
Theorem	eleq1a 2281	A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))
Theorem	eqeltri 2282	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ 𝐴 ∈ 𝐶
Theorem	eqeltrri 2283	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ 𝐵 ∈ 𝐶
Theorem	eleqtri 2284	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 ∈ 𝐶
Theorem	eleqtrri 2285	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 ∈ 𝐶
Theorem	eqeltrd 2286	Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrrd 2287	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝐶)
Theorem	eleqtrd 2288	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrrd 2289	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	3eltr3i 2290	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐶 ∈ 𝐷
Theorem	3eltr4i 2291	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐶 ∈ 𝐷
Theorem	3eltr3d 2292	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	3eltr4d 2293	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	3eltr3g 2294	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	3eltr4g 2295	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
Theorem	eqeltrid 2296	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrrid 2297	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrid 2298	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrrid 2299	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eqeltrdi 2300	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)