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	eqriv 2201*	Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( x e. A <-> x e. B )   =>    |- A = B
Theorem	eqrdv 2202*	Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
|- ( ph -> ( x e. A <-> x e. B ) )   =>    |- ( ph -> A = B )
Theorem	eqrdav 2203*	Deduce equality of classes from an equivalence of membership that depends on the membership variable. (Contributed by NM, 7-Nov-2008.)
|- ( ( ph /\ x e. A ) -> x e. C )   &    |- ( ( ph /\ x e. B ) -> x e. C )   &    |- ( ( ph /\ x e. C ) -> ( x e. A <-> x e. B ) )   =>    |- ( ph -> A = B )
Theorem	eqid 2204	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.)
|- A = A
Theorem	eqidd 2205	Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
|- ( ph -> A = A )
Theorem	eqcom 2206	Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)
|- ( A = B <-> B = A )
Theorem	eqcoms 2207	Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ph )   =>    |- ( B = A -> ph )
Theorem	eqcomi 2208	Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- B = A
Theorem	neqcomd 2209	Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> -. A = B )   =>    |- ( ph -> -. B = A )
Theorem	eqcomd 2210	Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)
|- ( ph -> A = B )   =>    |- ( ph -> B = A )
Theorem	eqeq1 2211	Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( A = C <-> B = C ) )
Theorem	eqeq1i 2212	Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( A = C <-> B = C )
Theorem	eqeq1d 2213	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A = C <-> B = C ) )
Theorem	eqeq2 2214	Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( C = A <-> C = B ) )
Theorem	eqeq2i 2215	Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( C = A <-> C = B )
Theorem	eqeq2d 2216	Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C = A <-> C = B ) )
Theorem	eqeq12 2217	Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.)
|- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) )
Theorem	eqeq12i 2218	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 2219	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 2220	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 2221	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 2222	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 2223	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 2224	A transitive law for class equality. (Contributed by NM, 20-May-2005.)
|- ( ( A = C /\ B = C ) -> A = B )
Theorem	eqtri 2225	An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B = C   =>    |- A = C
Theorem	eqtr2i 2226	An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
|- A = B   &    |- B = C   =>    |- C = A
Theorem	eqtr3i 2227	An equality transitivity inference. (Contributed by NM, 6-May-1994.)
|- A = B   &    |- A = C   =>    |- B = C
Theorem	eqtr4i 2228	An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- C = B   =>    |- A = C
Theorem	3eqtri 2229	An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
|- A = B   &    |- B = C   &    |- C = D   =>    |- A = D
Theorem	3eqtrri 2230	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 2231	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
|- A = B   &    |- C = B   &    |- C = D   =>    |- A = D
Theorem	3eqtr2ri 2232	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 2233	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 2234	An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
|- A = B   &    |- A = C   &    |- B = D   =>    |- D = C
Theorem	3eqtr4i 2235	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 2236	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 2237	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	eqtr2d 2238	An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
|- ( ph -> A = B )   &    |- ( ph -> B = C )   =>    |- ( ph -> C = A )
Theorem	eqtr3d 2239	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
|- ( ph -> A = B )   &    |- ( ph -> A = C )   =>    |- ( ph -> B = C )
Theorem	eqtr4d 2240	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
|- ( ph -> A = B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A = C )
Theorem	3eqtrd 2241	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 2242	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 2243	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 2244	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 2245	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 2246	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 2247	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 2248	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 2249	An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
|- A = B   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	eqtr2id 2250	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- A = B   &    |- ( ph -> B = C )   =>    |- ( ph -> C = A )
Theorem	eqtr3id 2251	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- B = A   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	eqtr3di 2252	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- ( ph -> A = B )   &    |- A = C   =>    |- ( ph -> B = C )
Theorem	eqtrdi 2253	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- B = C   =>    |- ( ph -> A = C )
Theorem	eqtr2di 2254	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- ( ph -> A = B )   &    |- B = C   =>    |- ( ph -> C = A )
Theorem	eqtr4di 2255	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- C = B   =>    |- ( ph -> A = C )
Theorem	eqtr4id 2256	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- A = B   &    |- ( ph -> C = B )   =>    |- ( ph -> A = C )
Theorem	sylan9eq 2257	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 2258	An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
|- ( ph -> B = A )   &    |- ( ps -> B = C )   =>    |- ( ( ph /\ ps ) -> A = C )
Theorem	sylan9eqr 2259	An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
|- ( ph -> A = B )   &    |- ( ps -> B = C )   =>    |- ( ( ps /\ ph ) -> A = C )
Theorem	3eqtr3g 2260	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 2261	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 2262	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 2263	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 2264	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 2265	Weaker version of eleq1 2267 (but more general than elequ1 2179) not depending on ax-ext 2186 nor df-cleq 2197. (Contributed by BJ, 24-Jun-2019.)
|- ( x = y -> ( x e. A <-> y e. A ) )
Theorem	eleq2w 2266	Weaker version of eleq2 2268 (but more general than elequ2 2180) not depending on ax-ext 2186 nor df-cleq 2197. (Contributed by BJ, 29-Sep-2019.)
|- ( x = y -> ( A e. x <-> A e. y ) )
Theorem	eleq1 2267	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( A e. C <-> B e. C ) )
Theorem	eleq2 2268	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( C e. A <-> C e. B ) )
Theorem	eleq12 2269	Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
|- ( ( A = B /\ C = D ) -> ( A e. C <-> B e. D ) )
Theorem	eleq1i 2270	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( A e. C <-> B e. C )
Theorem	eleq2i 2271	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( C e. A <-> C e. B )
Theorem	eleq12i 2272	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 2273	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 2274	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 2275	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 2276	A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
|- ( A e. B -> ( C = A -> C e. B ) )
Theorem	eqeltri 2277	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B e. C   =>    |- A e. C
Theorem	eqeltrri 2278	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- A e. C   =>    |- B e. C
Theorem	eleqtri 2279	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- B = C   =>    |- A e. C
Theorem	eleqtrri 2280	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- C = B   =>    |- A e. C
Theorem	eqeltrd 2281	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 2282	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 2283	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 2284	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 2285	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 2286	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 2287	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 2288	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 2289	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 2290	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 2291	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A = B   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	eqeltrrid 2292	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- B = A   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	eleqtrid 2293	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> B = C )   =>    |- ( ph -> A e. C )
Theorem	eleqtrrid 2294	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> C = B )   =>    |- ( ph -> A e. C )
Theorem	eqeltrdi 2295	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A = B )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	eqeltrrdi 2296	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> B = A )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	eleqtrdi 2297	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A e. B )   &    |- B = C   =>    |- ( ph -> A e. C )
Theorem	eleqtrrdi 2298	A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
|- ( ph -> A e. B )   &    |- C = B   =>    |- ( ph -> A e. C )
Theorem	eleq2s 2299	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 2300	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 )