P. 22 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2101-2200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eqeq12i 2101	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 2102	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 2103	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 2104	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 2105	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 2106	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 2107	A transitive law for class equality. (Contributed by NM, 20-May-2005.)
|- ( ( A = C /\ B = C ) -> A = B )
Theorem	eqtri 2108	An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B = C   =>    |- A = C
Theorem	eqtr2i 2109	An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
|- A = B   &    |- B = C   =>    |- C = A
Theorem	eqtr3i 2110	An equality transitivity inference. (Contributed by NM, 6-May-1994.)
|- A = B   &    |- A = C   =>    |- B = C
Theorem	eqtr4i 2111	An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- C = B   =>    |- A = C
Theorem	3eqtri 2112	An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
|- A = B   &    |- B = C   &    |- C = D   =>    |- A = D
Theorem	3eqtrri 2113	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 2114	An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
|- A = B   &    |- C = B   &    |- C = D   =>    |- A = D
Theorem	3eqtr2ri 2115	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 2116	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 2117	An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
|- A = B   &    |- A = C   &    |- B = D   =>    |- D = C
Theorem	3eqtr4i 2118	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 2119	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 2120	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	eqtr2d 2121	An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
|- ( ph -> A = B )   &    |- ( ph -> B = C )   =>    |- ( ph -> C = A )
Theorem	eqtr3d 2122	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
|- ( ph -> A = B )   &    |- ( ph -> A = C )   =>    |- ( ph -> B = C )
Theorem	eqtr4d 2123	An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
|- ( ph -> A = B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A = C )
Theorem	3eqtrd 2124	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 2125	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 2126	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 2127	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 2128	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 2129	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 2130	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 2131	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	syl5eq 2132	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	syl5req 2133	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- A = B   &    |- ( ph -> B = C )   =>    |- ( ph -> C = A )
Theorem	syl5eqr 2134	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- B = A   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	syl5reqr 2135	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- B = A   &    |- ( ph -> B = C )   =>    |- ( ph -> C = A )
Theorem	syl6eq 2136	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- B = C   =>    |- ( ph -> A = C )
Theorem	syl6req 2137	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- ( ph -> A = B )   &    |- B = C   =>    |- ( ph -> C = A )
Theorem	syl6eqr 2138	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- C = B   =>    |- ( ph -> A = C )
Theorem	syl6reqr 2139	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- ( ph -> A = B )   &    |- C = B   =>    |- ( ph -> C = A )
Theorem	sylan9eq 2140	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 2141	An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
|- ( ph -> B = A )   &    |- ( ps -> B = C )   =>    |- ( ( ph /\ ps ) -> A = C )
Theorem	sylan9eqr 2142	An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
|- ( ph -> A = B )   &    |- ( ps -> B = C )   =>    |- ( ( ps /\ ph ) -> A = C )
Theorem	3eqtr3g 2143	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 2144	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 2145	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 2146	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 2147	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 2148	Weaker version of eleq1 2150 (but more general than elequ1 1647) not depending on ax-ext 2070 nor df-cleq 2081. (Contributed by BJ, 24-Jun-2019.)
|- ( x = y -> ( x e. A <-> y e. A ) )
Theorem	eleq2w 2149	Weaker version of eleq2 2151 (but more general than elequ2 1648) not depending on ax-ext 2070 nor df-cleq 2081. (Contributed by BJ, 29-Sep-2019.)
|- ( x = y -> ( A e. x <-> A e. y ) )
Theorem	eleq1 2150	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( A e. C <-> B e. C ) )
Theorem	eleq2 2151	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( C e. A <-> C e. B ) )
Theorem	eleq12 2152	Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
|- ( ( A = B /\ C = D ) -> ( A e. C <-> B e. D ) )
Theorem	eleq1i 2153	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( A e. C <-> B e. C )
Theorem	eleq2i 2154	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( C e. A <-> C e. B )
Theorem	eleq12i 2155	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 2156	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 2157	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 2158	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 2159	A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
|- ( A e. B -> ( C = A -> C e. B ) )
Theorem	eqeltri 2160	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B e. C   =>    |- A e. C
Theorem	eqeltrri 2161	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- A e. C   =>    |- B e. C
Theorem	eleqtri 2162	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- B = C   =>    |- A e. C
Theorem	eleqtrri 2163	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- C = B   =>    |- A e. C
Theorem	eqeltrd 2164	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 2165	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 2166	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 2167	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 2168	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 2169	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 2170	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 2171	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 2172	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 2173	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	syl5eqel 2174	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A = B   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	syl5eqelr 2175	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- B = A   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	syl5eleq 2176	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> B = C )   =>    |- ( ph -> A e. C )
Theorem	syl5eleqr 2177	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> C = B )   =>    |- ( ph -> A e. C )
Theorem	syl6eqel 2178	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A = B )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	syl6eqelr 2179	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> B = A )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	syl6eleq 2180	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A e. B )   &    |- B = C   =>    |- ( ph -> A e. C )
Theorem	syl6eleqr 2181	A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
|- ( ph -> A e. B )   &    |- C = B   =>    |- ( ph -> A e. C )
Theorem	eleq2s 2182	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 2183	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 2184	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 2185	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 2186	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 2187*	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2252. (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 2188	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 2189	A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.)
|- ( ( A e. B /\ -. A e. C ) -> -. B = C )
Theorem	eqsb3lem 2190*	Lemma for eqsb3 2191. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( [ x / y ] y = A <-> x = A )
Theorem	eqsb3 2191*	Substitution applied to an atomic wff (class version of equsb3 1873). (Contributed by Rodolfo Medina, 28-Apr-2010.)
|- ( [ x / y ] y = A <-> x = A )
Theorem	clelsb3 2192*	Substitution applied to an atomic wff (class version of elsb3 1900). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( [ x / y ] y e. A <-> x e. A )
Theorem	clelsb4 2193*	Substitution applied to an atomic wff (class version of elsb4 1901). (Contributed by Jim Kingdon, 22-Nov-2018.)
|- ( [ x / y ] A e. y <-> A e. x )
Theorem	hbxfreq 2194	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1406 for equivalence version. (Contributed by NM, 21-Aug-2007.)
|- A = B   &    |- ( y e. B -> A. x y e. B )   =>    |- ( y e. A -> A. x y e. A )
Theorem	hblem 2195*	Change the free variable of a hypothesis builder. (Contributed by NM, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.)
|- ( y e. A -> A. x y e. A )   =>    |- ( z e. A -> A. x z e. A )
Theorem	abeq2 2196*	Equality of a class variable and a class abstraction (also called a class builder). Theorem 5.1 of [Quine] p. 34. This theorem shows the relationship between expressions with class abstractions and expressions with class variables. Note that abbi 2201 and its relatives are among those useful for converting theorems with class variables to equivalent theorems with wff variables, by first substituting a class abstraction for each class variable. Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable ph (that has a free variable x) to a theorem with a class variable A, we substitute x e. A for ph throughout and simplify, where A is a new class variable not already in the wff. Conversely, to convert a theorem with a class variable A to one with ph, we substitute { x | ph } for A throughout and simplify, where x and ph are new set and wff variables not already in the wff. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 5-Aug-1993.)
|- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) )
Theorem	abeq1 2197*	Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.)
|- ( { x | ph } = A <-> A. x ( ph <-> x e. A ) )
Theorem	abeq2i 2198	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.)
|- A = { x | ph }   =>    |- ( x e. A <-> ph )
Theorem	abeq1i 2199	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 31-Jul-1994.)
|- { x | ph } = A   =>    |- ( ph <-> x e. A )
Theorem	abeq2d 2200	Equality of a class variable and a class abstraction (deduction). (Contributed by NM, 16-Nov-1995.)
|- ( ph -> A = { x | ps } )   =>    |- ( ph -> ( x e. A <-> ps ) )