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	neqcomd 2201	Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> -. A = B )   =>    |- ( ph -> -. B = A )
Theorem	eqcomd 2202	Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)
|- ( ph -> A = B )   =>    |- ( ph -> B = A )
Theorem	eqeq1 2203	Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( A = C <-> B = C ) )
Theorem	eqeq1i 2204	Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( A = C <-> B = C )
Theorem	eqeq1d 2205	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A = C <-> B = C ) )
Theorem	eqeq2 2206	Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( C = A <-> C = B ) )
Theorem	eqeq2i 2207	Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( C = A <-> C = B )
Theorem	eqeq2d 2208	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C = A <-> C = B ) )
Theorem	eqeq12 2209	Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.)
|- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) )
Theorem	eqeq12i 2210	A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- A = B   &    |- C = D   =>    |- ( A = C <-> B = D )
Theorem	eqeq12d 2211	A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A = C <-> B = D ) )
Theorem	eqeqan12d 2212	A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ph /\ ps ) -> ( A = C <-> B = D ) )
Theorem	eqeqan12rd 2213	A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ps /\ ph ) -> ( A = C <-> B = D ) )
Theorem	eqtr 2214	Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
|- ( ( A = B /\ B = C ) -> A = C )
Theorem	eqtr2 2215	A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ( A = B /\ A = C ) -> B = C )
Theorem	eqtr3 2216	A transitive law for class equality. (Contributed by NM, 20-May-2005.)
|- ( ( A = C /\ B = C ) -> A = B )
Theorem	eqtri 2217	An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B = C   =>    |- A = C
Theorem	eqtr2i 2218	An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
|- A = B   &    |- B = C   =>    |- C = A
Theorem	eqtr3i 2219	An equality transitivity inference. (Contributed by NM, 6-May-1994.)
|- A = B   &    |- A = C   =>    |- B = C
Theorem	eqtr4i 2220	An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- C = B   =>    |- A = C
Theorem	3eqtri 2221	An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
|- A = B   &    |- B = C   &    |- C = D   =>    |- A = D
Theorem	3eqtrri 2222	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- A = B   &    |- B = C   &    |- C = D   =>    |- D = A
Theorem	3eqtr2i 2223	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
|- A = B   &    |- C = B   &    |- C = D   =>    |- A = D
Theorem	3eqtr2ri 2224	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- A = B   &    |- C = B   &    |- C = D   =>    |- D = A
Theorem	3eqtr3i 2225	An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- A = B   &    |- A = C   &    |- B = D   =>    |- C = D
Theorem	3eqtr3ri 2226	An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
|- A = B   &    |- A = C   &    |- B = D   =>    |- D = C
Theorem	3eqtr4i 2227	An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- A = B   &    |- C = A   &    |- D = B   =>    |- C = D
Theorem	3eqtr4ri 2228	An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- A = B   &    |- C = A   &    |- D = B   =>    |- D = C
Theorem	eqtrd 2229	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	eqtr2d 2230	An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
|- ( ph -> A = B )   &    |- ( ph -> B = C )   =>    |- ( ph -> C = A )
Theorem	eqtr3d 2231	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
|- ( ph -> A = B )   &    |- ( ph -> A = C )   =>    |- ( ph -> B = C )
Theorem	eqtr4d 2232	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
|- ( ph -> A = B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A = C )
Theorem	3eqtrd 2233	A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
|- ( ph -> A = B )   &    |- ( ph -> B = C )   &    |- ( ph -> C = D )   =>    |- ( ph -> A = D )
Theorem	3eqtrrd 2234	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A = B )   &    |- ( ph -> B = C )   &    |- ( ph -> C = D )   =>    |- ( ph -> D = A )
Theorem	3eqtr2d 2235	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
|- ( ph -> A = B )   &    |- ( ph -> C = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> A = D )
Theorem	3eqtr2rd 2236	A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
|- ( ph -> A = B )   &    |- ( ph -> C = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> D = A )
Theorem	3eqtr3d 2237	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A = B )   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> C = D )
Theorem	3eqtr3rd 2238	A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
|- ( ph -> A = B )   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> D = C )
Theorem	3eqtr4d 2239	A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = A )   &    |- ( ph -> D = B )   =>    |- ( ph -> C = D )
Theorem	3eqtr4rd 2240	A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
|- ( ph -> A = B )   &    |- ( ph -> C = A )   &    |- ( ph -> D = B )   =>    |- ( ph -> D = C )
Theorem	eqtrid 2241	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
|- A = B   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	eqtr2id 2242	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- A = B   &    |- ( ph -> B = C )   =>    |- ( ph -> C = A )
Theorem	eqtr3id 2243	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- B = A   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	eqtr3di 2244	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- ( ph -> A = B )   &    |- A = C   =>    |- ( ph -> B = C )
Theorem	eqtrdi 2245	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- B = C   =>    |- ( ph -> A = C )
Theorem	eqtr2di 2246	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- ( ph -> A = B )   &    |- B = C   =>    |- ( ph -> C = A )
Theorem	eqtr4di 2247	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- C = B   =>    |- ( ph -> A = C )
Theorem	eqtr4id 2248	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- A = B   &    |- ( ph -> C = B )   =>    |- ( ph -> A = C )
Theorem	sylan9eq 2249	An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A = B )   &    |- ( ps -> B = C )   =>    |- ( ( ph /\ ps ) -> A = C )
Theorem	sylan9req 2250	An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
|- ( ph -> B = A )   &    |- ( ps -> B = C )   =>    |- ( ( ph /\ ps ) -> A = C )
Theorem	sylan9eqr 2251	An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
|- ( ph -> A = B )   &    |- ( ps -> B = C )   =>    |- ( ( ps /\ ph ) -> A = C )
Theorem	3eqtr3g 2252	A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
|- ( ph -> A = B )   &    |- A = C   &    |- B = D   =>    |- ( ph -> C = D )
Theorem	3eqtr3a 2253	A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
|- A = B   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> C = D )
Theorem	3eqtr4g 2254	A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- C = A   &    |- D = B   =>    |- ( ph -> C = D )
Theorem	3eqtr4a 2255	A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- A = B   &    |- ( ph -> C = A )   &    |- ( ph -> D = B )   =>    |- ( ph -> C = D )
Theorem	eq2tri 2256	A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
|- ( A = C -> D = F )   &    |- ( B = D -> C = G )   =>    |- ( ( A = C /\ B = F ) <-> ( B = D /\ A = G ) )
Theorem	eleq1w 2257	Weaker version of eleq1 2259 (but more general than elequ1 2171) not depending on ax-ext 2178 nor df-cleq 2189. (Contributed by BJ, 24-Jun-2019.)
|- ( x = y -> ( x e. A <-> y e. A ) )
Theorem	eleq2w 2258	Weaker version of eleq2 2260 (but more general than elequ2 2172) not depending on ax-ext 2178 nor df-cleq 2189. (Contributed by BJ, 29-Sep-2019.)
|- ( x = y -> ( A e. x <-> A e. y ) )
Theorem	eleq1 2259	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( A e. C <-> B e. C ) )
Theorem	eleq2 2260	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( C e. A <-> C e. B ) )
Theorem	eleq12 2261	Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
|- ( ( A = B /\ C = D ) -> ( A e. C <-> B e. D ) )
Theorem	eleq1i 2262	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( A e. C <-> B e. C )
Theorem	eleq2i 2263	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( C e. A <-> C e. B )
Theorem	eleq12i 2264	Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
|- A = B   &    |- C = D   =>    |- ( A e. C <-> B e. D )
Theorem	eleq1d 2265	Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A e. C <-> B e. C ) )
Theorem	eleq2d 2266	Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C e. A <-> C e. B ) )
Theorem	eleq12d 2267	Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A e. C <-> B e. D ) )
Theorem	eleq1a 2268	A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
|- ( A e. B -> ( C = A -> C e. B ) )
Theorem	eqeltri 2269	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B e. C   =>    |- A e. C
Theorem	eqeltrri 2270	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- A e. C   =>    |- B e. C
Theorem	eleqtri 2271	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- B = C   =>    |- A e. C
Theorem	eleqtrri 2272	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- C = B   =>    |- A e. C
Theorem	eqeltrd 2273	Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
|- ( ph -> A = B )   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	eqeltrrd 2274	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
|- ( ph -> A = B )   &    |- ( ph -> A e. C )   =>    |- ( ph -> B e. C )
Theorem	eleqtrd 2275	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
|- ( ph -> A e. B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A e. C )
Theorem	eleqtrrd 2276	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
|- ( ph -> A e. B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A e. C )
Theorem	3eltr3i 2277	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- A e. B   &    |- A = C   &    |- B = D   =>    |- C e. D
Theorem	3eltr4i 2278	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- A e. B   &    |- C = A   &    |- D = B   =>    |- C e. D
Theorem	3eltr3d 2279	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> A e. B )   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> C e. D )
Theorem	3eltr4d 2280	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> A e. B )   &    |- ( ph -> C = A )   &    |- ( ph -> D = B )   =>    |- ( ph -> C e. D )
Theorem	3eltr3g 2281	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> A e. B )   &    |- A = C   &    |- B = D   =>    |- ( ph -> C e. D )
Theorem	3eltr4g 2282	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> A e. B )   &    |- C = A   &    |- D = B   =>    |- ( ph -> C e. D )
Theorem	eqeltrid 2283	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A = B   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	eqeltrrid 2284	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- B = A   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	eleqtrid 2285	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> B = C )   =>    |- ( ph -> A e. C )
Theorem	eleqtrrid 2286	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> C = B )   =>    |- ( ph -> A e. C )
Theorem	eqeltrdi 2287	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A = B )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	eqeltrrdi 2288	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> B = A )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	eleqtrdi 2289	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A e. B )   &    |- B = C   =>    |- ( ph -> A e. C )
Theorem	eleqtrrdi 2290	A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
|- ( ph -> A e. B )   &    |- C = B   =>    |- ( ph -> A e. C )
Theorem	eleq2s 2291	Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( A e. B -> ph )   &    |- C = B   =>    |- ( A e. C -> ph )
Theorem	eqneltrd 2292	If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A = B )   &    |- ( ph -> -. B e. C )   =>    |- ( ph -> -. A e. C )
Theorem	eqneltrrd 2293	If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A = B )   &    |- ( ph -> -. A e. C )   =>    |- ( ph -> -. B e. C )
Theorem	neleqtrd 2294	If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> -. C e. A )   &    |- ( ph -> A = B )   =>    |- ( ph -> -. C e. B )
Theorem	neleqtrrd 2295	If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> -. C e. B )   &    |- ( ph -> A = B )   =>    |- ( ph -> -. C e. A )
Theorem	cleqh 2296*	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2364. (Contributed by NM, 5-Aug-1993.)
|- ( y e. A -> A. x y e. A )   &    |- ( y e. B -> A. x y e. B )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
Theorem	nelneq 2297	A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.)
|- ( ( A e. C /\ -. B e. C ) -> -. A = B )
Theorem	nelneq2 2298	A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.)
|- ( ( A e. B /\ -. A e. C ) -> -. B = C )
Theorem	eqsb1lem 2299*	Lemma for eqsb1 2300. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( [ y / x ] x = A <-> y = A )
Theorem	eqsb1 2300*	Substitution for the left-hand side in an equality. Class version of equsb3 1970. (Contributed by Rodolfo Medina, 28-Apr-2010.)
|- ( [ y / x ] x = A <-> y = A )