HomeHome Intuitionistic Logic Explorer
Theorem List (p. 22 of 131)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 2101-2200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
2.1.2  Class abstractions (a.k.a. class builders)
 
Syntaxcab 2101 Introduce the class builder or class abstraction notation ("the class of sets 𝑥 such that 𝜑 is true"). Our class variables 𝐴, 𝐵, etc. range over class builders (sometimes implicitly). Note that a setvar variable can be expressed as a class builder per theorem cvjust 2110, justifying the assignment of setvar variables to class variables via the use of cv 1313.
class {𝑥𝜑}
 
Definitiondf-clab 2102 Define class abstraction notation (so-called by Quine), also called a "class builder" in the literature. 𝑥 and 𝑦 need not be distinct. Definition 2.1 of [Quine] p. 16. Typically, 𝜑 will have 𝑦 as a free variable, and "{𝑦𝜑} " is read "the class of all sets 𝑦 such that 𝜑(𝑦) is true." We do not define {𝑦𝜑} in isolation but only as part of an expression that extends or "overloads" the relationship.

This is our first use of the symbol to connect classes instead of sets. The syntax definition wcel 1463, which extends or "overloads" the wel 1464 definition connecting setvar variables, requires that both sides of be a class. In df-cleq 2108 and df-clel 2111, we introduce a new kind of variable (class variable) that can substituted with expressions such as {𝑦𝜑}. In the present definition, the 𝑥 on the left-hand side is a setvar variable. Syntax definition cv 1313 allows us to substitute a setvar variable 𝑥 for a class variable: all sets are classes by cvjust 2110 (but not necessarily vice-versa). For a full description of how classes are introduced and how to recover the primitive language, see the discussion in Quine (and under abeq2 2224 for a quick overview).

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 called the "axiom of class comprehension" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. He calls the construction {𝑦𝜑} a "class term".

For a general discussion of the theory of classes, see https://us.metamath.org/mpeuni/mmset.html#class 2224. (Contributed by NM, 5-Aug-1993.)

(𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
 
Theoremabid 2103 Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 5-Aug-1993.)
(𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
 
Theoremhbab1 2104* Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 5-Aug-1993.)
(𝑦 ∈ {𝑥𝜑} → ∀𝑥 𝑦 ∈ {𝑥𝜑})
 
Theoremnfsab1 2105* Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥 𝑦 ∈ {𝑥𝜑}
 
Theoremhbab 2106* Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 1-Mar-1995.)
(𝜑 → ∀𝑥𝜑)       (𝑧 ∈ {𝑦𝜑} → ∀𝑥 𝑧 ∈ {𝑦𝜑})
 
Theoremnfsab 2107* Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥𝜑       𝑥 𝑧 ∈ {𝑦𝜑}
 
Definitiondf-cleq 2108* 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 2099). 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 2102, df-clel 2111, and abeq2 2224.

In the form of dfcleq 2109, 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 2109. (Contributed by NM, 15-Sep-1993.)

(∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)       (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
 
Theoremdfcleq 2109* The same as df-cleq 2108 with the hypothesis removed using the Axiom of Extensionality ax-ext 2097. (Contributed by NM, 15-Sep-1993.)
(𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
 
Theoremcvjust 2110* 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 1313, which allows us to substitute a setvar variable for a class variable. See also cab 2101 and df-clab 2102. Note that this is not a rigorous justification, because cv 1313 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.)
𝑥 = {𝑦𝑦𝑥}
 
Definitiondf-clel 2111* 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 2108 it extends or "overloads" the use of the existing membership symbol, but unlike df-cleq 2108 it does not strengthen the set of valid wffs of logic when the class variables are replaced with setvar variables (see cleljust 1888), so we don't include any set theory axiom as a hypothesis. See also comments about the syntax under df-clab 2102.

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 2102. (Contributed by NM, 5-Aug-1993.)

(𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
 
Theoremeqriv 2112* Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)
(𝑥𝐴𝑥𝐵)       𝐴 = 𝐵
 
Theoremeqrdv 2113* Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
(𝜑 → (𝑥𝐴𝑥𝐵))       (𝜑𝐴 = 𝐵)
 
Theoremeqrdav 2114* Deduce equality of classes from an equivalence of membership that depends on the membership variable. (Contributed by NM, 7-Nov-2008.)
((𝜑𝑥𝐴) → 𝑥𝐶)    &   ((𝜑𝑥𝐵) → 𝑥𝐶)    &   ((𝜑𝑥𝐶) → (𝑥𝐴𝑥𝐵))       (𝜑𝐴 = 𝐵)
 
Theoremeqid 2115 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.)

𝐴 = 𝐴
 
Theoremeqidd 2116 Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
(𝜑𝐴 = 𝐴)
 
Theoremeqcom 2117 Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)
(𝐴 = 𝐵𝐵 = 𝐴)
 
Theoremeqcoms 2118 Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)
(𝐴 = 𝐵𝜑)       (𝐵 = 𝐴𝜑)
 
Theoremeqcomi 2119 Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵       𝐵 = 𝐴
 
Theoremneqcomd 2120 Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.)
(𝜑 → ¬ 𝐴 = 𝐵)       (𝜑 → ¬ 𝐵 = 𝐴)
 
Theoremeqcomd 2121 Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)
(𝜑𝐴 = 𝐵)       (𝜑𝐵 = 𝐴)
 
Theoremeqeq1 2122 Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
(𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
 
Theoremeqeq1i 2123 Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵       (𝐴 = 𝐶𝐵 = 𝐶)
 
Theoremeqeq1d 2124 Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐴 = 𝐶𝐵 = 𝐶))
 
Theoremeqeq2 2125 Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
(𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
 
Theoremeqeq2i 2126 Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵       (𝐶 = 𝐴𝐶 = 𝐵)
 
Theoremeqeq2d 2127 Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
 
Theoremeqeq12 2128 Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.)
((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
 
Theoremeqeq12i 2129 A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐶 = 𝐷       (𝐴 = 𝐶𝐵 = 𝐷)
 
Theoremeqeq12d 2130 A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
 
Theoremeqeqan12d 2131 A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐶 = 𝐷)       ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))
 
Theoremeqeqan12rd 2132 A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐶 = 𝐷)       ((𝜓𝜑) → (𝐴 = 𝐶𝐵 = 𝐷))
 
Theoremeqtr 2133 Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
 
Theoremeqtr2 2134 A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
((𝐴 = 𝐵𝐴 = 𝐶) → 𝐵 = 𝐶)
 
Theoremeqtr3 2135 A transitive law for class equality. (Contributed by NM, 20-May-2005.)
((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
 
Theoremeqtri 2136 An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐵 = 𝐶       𝐴 = 𝐶
 
Theoremeqtr2i 2137 An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
𝐴 = 𝐵    &   𝐵 = 𝐶       𝐶 = 𝐴
 
Theoremeqtr3i 2138 An equality transitivity inference. (Contributed by NM, 6-May-1994.)
𝐴 = 𝐵    &   𝐴 = 𝐶       𝐵 = 𝐶
 
Theoremeqtr4i 2139 An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐶 = 𝐵       𝐴 = 𝐶
 
Theorem3eqtri 2140 An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
𝐴 = 𝐵    &   𝐵 = 𝐶    &   𝐶 = 𝐷       𝐴 = 𝐷
 
Theorem3eqtrri 2141 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐵 = 𝐶    &   𝐶 = 𝐷       𝐷 = 𝐴
 
Theorem3eqtr2i 2142 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
𝐴 = 𝐵    &   𝐶 = 𝐵    &   𝐶 = 𝐷       𝐴 = 𝐷
 
Theorem3eqtr2ri 2143 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐶 = 𝐵    &   𝐶 = 𝐷       𝐷 = 𝐴
 
Theorem3eqtr3i 2144 An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐴 = 𝐶    &   𝐵 = 𝐷       𝐶 = 𝐷
 
Theorem3eqtr3ri 2145 An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
𝐴 = 𝐵    &   𝐴 = 𝐶    &   𝐵 = 𝐷       𝐷 = 𝐶
 
Theorem3eqtr4i 2146 An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐶 = 𝐴    &   𝐷 = 𝐵       𝐶 = 𝐷
 
Theorem3eqtr4ri 2147 An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐶 = 𝐴    &   𝐷 = 𝐵       𝐷 = 𝐶
 
Theoremeqtrd 2148 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴 = 𝐶)
 
Theoremeqtr2d 2149 An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵 = 𝐶)       (𝜑𝐶 = 𝐴)
 
Theoremeqtr3d 2150 An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴 = 𝐶)       (𝜑𝐵 = 𝐶)
 
Theoremeqtr4d 2151 An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴 = 𝐶)
 
Theorem3eqtrd 2152 A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵 = 𝐶)    &   (𝜑𝐶 = 𝐷)       (𝜑𝐴 = 𝐷)
 
Theorem3eqtrrd 2153 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵 = 𝐶)    &   (𝜑𝐶 = 𝐷)       (𝜑𝐷 = 𝐴)
 
Theorem3eqtr2d 2154 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑𝐴 = 𝐷)
 
Theorem3eqtr2rd 2155 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑𝐷 = 𝐴)
 
Theorem3eqtr3d 2156 A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐶 = 𝐷)
 
Theorem3eqtr3rd 2157 A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐷 = 𝐶)
 
Theorem3eqtr4d 2158 A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐶 = 𝐷)
 
Theorem3eqtr4rd 2159 A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐷 = 𝐶)
 
Theoremsyl5eq 2160 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴 = 𝐶)
 
Theoremsyl5req 2161 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
𝐴 = 𝐵    &   (𝜑𝐵 = 𝐶)       (𝜑𝐶 = 𝐴)
 
Theoremsyl5eqr 2162 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
𝐵 = 𝐴    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴 = 𝐶)
 
Theoremsyl5reqr 2163 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
𝐵 = 𝐴    &   (𝜑𝐵 = 𝐶)       (𝜑𝐶 = 𝐴)
 
Theoremsyl6eq 2164 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
(𝜑𝐴 = 𝐵)    &   𝐵 = 𝐶       (𝜑𝐴 = 𝐶)
 
Theoremsyl6req 2165 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
(𝜑𝐴 = 𝐵)    &   𝐵 = 𝐶       (𝜑𝐶 = 𝐴)
 
Theoremsyl6eqr 2166 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
(𝜑𝐴 = 𝐵)    &   𝐶 = 𝐵       (𝜑𝐴 = 𝐶)
 
Theoremsyl6reqr 2167 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
(𝜑𝐴 = 𝐵)    &   𝐶 = 𝐵       (𝜑𝐶 = 𝐴)
 
Theoremsylan9eq 2168 An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐵 = 𝐶)       ((𝜑𝜓) → 𝐴 = 𝐶)
 
Theoremsylan9req 2169 An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
(𝜑𝐵 = 𝐴)    &   (𝜓𝐵 = 𝐶)       ((𝜑𝜓) → 𝐴 = 𝐶)
 
Theoremsylan9eqr 2170 An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐵 = 𝐶)       ((𝜓𝜑) → 𝐴 = 𝐶)
 
Theorem3eqtr3g 2171 A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
(𝜑𝐴 = 𝐵)    &   𝐴 = 𝐶    &   𝐵 = 𝐷       (𝜑𝐶 = 𝐷)
 
Theorem3eqtr3a 2172 A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
𝐴 = 𝐵    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐶 = 𝐷)
 
Theorem3eqtr4g 2173 A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)
(𝜑𝐴 = 𝐵)    &   𝐶 = 𝐴    &   𝐷 = 𝐵       (𝜑𝐶 = 𝐷)
 
Theorem3eqtr4a 2174 A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐶 = 𝐷)
 
Theoremeq2tri 2175 A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
(𝐴 = 𝐶𝐷 = 𝐹)    &   (𝐵 = 𝐷𝐶 = 𝐺)       ((𝐴 = 𝐶𝐵 = 𝐹) ↔ (𝐵 = 𝐷𝐴 = 𝐺))
 
Theoremeleq1w 2176 Weaker version of eleq1 2178 (but more general than elequ1 1673) not depending on ax-ext 2097 nor df-cleq 2108. (Contributed by BJ, 24-Jun-2019.)
(𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
 
Theoremeleq2w 2177 Weaker version of eleq2 2179 (but more general than elequ2 1674) not depending on ax-ext 2097 nor df-cleq 2108. (Contributed by BJ, 29-Sep-2019.)
(𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
 
Theoremeleq1 2178 Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
(𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
 
Theoremeleq2 2179 Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
(𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
 
Theoremeleq12 2180 Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶𝐵𝐷))
 
Theoremeleq1i 2181 Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵       (𝐴𝐶𝐵𝐶)
 
Theoremeleq2i 2182 Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵       (𝐶𝐴𝐶𝐵)
 
Theoremeleq12i 2183 Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
𝐴 = 𝐵    &   𝐶 = 𝐷       (𝐴𝐶𝐵𝐷)
 
Theoremeleq1d 2184 Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐴𝐶𝐵𝐶))
 
Theoremeleq2d 2185 Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶𝐴𝐶𝐵))
 
Theoremeleq12d 2186 Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴𝐶𝐵𝐷))
 
Theoremeleq1a 2187 A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
(𝐴𝐵 → (𝐶 = 𝐴𝐶𝐵))
 
Theoremeqeltri 2188 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐵𝐶       𝐴𝐶
 
Theoremeqeltrri 2189 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐴𝐶       𝐵𝐶
 
Theoremeleqtri 2190 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
𝐴𝐵    &   𝐵 = 𝐶       𝐴𝐶
 
Theoremeleqtrri 2191 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
𝐴𝐵    &   𝐶 = 𝐵       𝐴𝐶
 
Theoremeqeltrd 2192 Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)
 
Theoremeqeltrrd 2193 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴𝐶)       (𝜑𝐵𝐶)
 
Theoremeleqtrd 2194 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
(𝜑𝐴𝐵)    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴𝐶)
 
Theoremeleqtrrd 2195 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
(𝜑𝐴𝐵)    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴𝐶)
 
Theorem3eltr3i 2196 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
𝐴𝐵    &   𝐴 = 𝐶    &   𝐵 = 𝐷       𝐶𝐷
 
Theorem3eltr4i 2197 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
𝐴𝐵    &   𝐶 = 𝐴    &   𝐷 = 𝐵       𝐶𝐷
 
Theorem3eltr3d 2198 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
(𝜑𝐴𝐵)    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐶𝐷)
 
Theorem3eltr4d 2199 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
(𝜑𝐴𝐵)    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐶𝐷)
 
Theorem3eltr3g 2200 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
(𝜑𝐴𝐵)    &   𝐴 = 𝐶    &   𝐵 = 𝐷       (𝜑𝐶𝐷)
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13088
  Copyright terms: Public domain < Previous  Next >