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	3eqtr4rd 2201	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 2202	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	syl5req 2203	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- A = B   &    |- ( ph -> B = C )   =>    |- ( ph -> C = A )
Theorem	syl5eqr 2204	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- B = A   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	syl5reqr 2205	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- B = A   &    |- ( ph -> B = C )   =>    |- ( ph -> C = A )
Theorem	eqtrdi 2206	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- B = C   =>    |- ( ph -> A = C )
Theorem	eqtr2di 2207	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- ( ph -> A = B )   &    |- B = C   =>    |- ( ph -> C = A )
Theorem	eqtr4di 2208	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A = B )   &    |- C = B   =>    |- ( ph -> A = C )
Theorem	eqtr4id 2209	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- A = B   &    |- ( ph -> C = B )   =>    |- ( ph -> A = C )
Theorem	sylan9eq 2210	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 2211	An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
|- ( ph -> B = A )   &    |- ( ps -> B = C )   =>    |- ( ( ph /\ ps ) -> A = C )
Theorem	sylan9eqr 2212	An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
|- ( ph -> A = B )   &    |- ( ps -> B = C )   =>    |- ( ( ps /\ ph ) -> A = C )
Theorem	3eqtr3g 2213	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 2214	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 2215	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 2216	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 2217	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 2218	Weaker version of eleq1 2220 (but more general than elequ1 2132) not depending on ax-ext 2139 nor df-cleq 2150. (Contributed by BJ, 24-Jun-2019.)
|- ( x = y -> ( x e. A <-> y e. A ) )
Theorem	eleq2w 2219	Weaker version of eleq2 2221 (but more general than elequ2 2133) not depending on ax-ext 2139 nor df-cleq 2150. (Contributed by BJ, 29-Sep-2019.)
|- ( x = y -> ( A e. x <-> A e. y ) )
Theorem	eleq1 2220	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( A e. C <-> B e. C ) )
Theorem	eleq2 2221	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( C e. A <-> C e. B ) )
Theorem	eleq12 2222	Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
|- ( ( A = B /\ C = D ) -> ( A e. C <-> B e. D ) )
Theorem	eleq1i 2223	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( A e. C <-> B e. C )
Theorem	eleq2i 2224	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( C e. A <-> C e. B )
Theorem	eleq12i 2225	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 2226	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 2227	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 2228	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 2229	A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
|- ( A e. B -> ( C = A -> C e. B ) )
Theorem	eqeltri 2230	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B e. C   =>    |- A e. C
Theorem	eqeltrri 2231	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- A e. C   =>    |- B e. C
Theorem	eleqtri 2232	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- B = C   =>    |- A e. C
Theorem	eleqtrri 2233	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- C = B   =>    |- A e. C
Theorem	eqeltrd 2234	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 2235	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 2236	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 2237	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 2238	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 2239	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 2240	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 2241	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 2242	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 2243	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 2244	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A = B   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	eqeltrrid 2245	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- B = A   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	eleqtrid 2246	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> B = C )   =>    |- ( ph -> A e. C )
Theorem	eleqtrrid 2247	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> C = B )   =>    |- ( ph -> A e. C )
Theorem	eqeltrdi 2248	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A = B )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	eqeltrrdi 2249	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> B = A )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	eleqtrdi 2250	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A e. B )   &    |- B = C   =>    |- ( ph -> A e. C )
Theorem	eleqtrrdi 2251	A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
|- ( ph -> A e. B )   &    |- C = B   =>    |- ( ph -> A e. C )
Theorem	eleq2s 2252	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 2253	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 2254	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 2255	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 2256	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 2257*	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2324. (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 2258	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 2259	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 2260*	Lemma for eqsb3 2261. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( [ y / x ] x = A <-> y = A )
Theorem	eqsb3 2261*	Substitution applied to an atomic wff (class version of equsb3 1931). (Contributed by Rodolfo Medina, 28-Apr-2010.)
|- ( [ y / x ] x = A <-> y = A )
Theorem	clelsb3 2262*	Substitution applied to an atomic wff (class version of elsb3 2135). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( [ y / x ] x e. A <-> y e. A )
Theorem	clelsb4 2263*	Substitution applied to an atomic wff (class version of elsb4 2136). (Contributed by Jim Kingdon, 22-Nov-2018.)
|- ( [ y / x ] A e. x <-> A e. y )
Theorem	hbxfreq 2264	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1452 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 2265*	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 2266*	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 2271 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 2267*	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 2268	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 2269	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 2270	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 ) )
Theorem	abbi 2271	Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.)
|- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
Theorem	abbi2i 2272*	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 5-Aug-1993.)
|- ( x e. A <-> ph )   =>    |- A = { x | ph }
Theorem	abbii 2273	Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   =>    |- { x | ph } = { x | ps }
Theorem	abbid 2274	Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x | ps } = { x | ch } )
Theorem	abbidv 2275*	Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x | ps } = { x | ch } )
Theorem	abbi2dv 2276*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
|- ( ph -> ( x e. A <-> ps ) )   =>    |- ( ph -> A = { x | ps } )
Theorem	abbi1dv 2277*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
|- ( ph -> ( ps <-> x e. A ) )   =>    |- ( ph -> { x | ps } = A )
Theorem	abid2 2278*	A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)
|- { x | x e. A } = A
Theorem	sb8ab 2279	Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.)
|- F/ y ph   =>    |- { x | ph } = { y | [ y / x ] ph }
Theorem	cbvabw 2280*	Version of cbvab 2281 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
Theorem	cbvab 2281	Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
Theorem	cbvabv 2282*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
Theorem	clelab 2283*	Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.)
|- ( A e. { x | ph } <-> E. x ( x = A /\ ph ) )
Theorem	clabel 2284*	Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.)
|- ( { x | ph } e. A <-> E. y ( y e. A /\ A. x ( x e. y <-> ph ) ) )
Theorem	sbab 2285*	The right-hand side of the second equality is a way of representing proper substitution of y for x into a class variable. (Contributed by NM, 14-Sep-2003.)
|- ( x = y -> A = { z | [ y / x ] z e. A } )
2.1.3  Class form not-free predicate
Syntax	wnfc 2286	Extend wff definition to include the not-free predicate for classes.
wff F/_ x A
Theorem	nfcjust 2287*	Justification theorem for df-nfc 2288. (Contributed by Mario Carneiro, 13-Oct-2016.)
|- ( A. y F/ x y e. A <-> A. z F/ x z e. A )
Definition	df-nfc 2288*	Define the not-free predicate for classes. This is read " x is not free in A". Not-free means that the value of x cannot affect the value of A, e.g., any occurrence of x in A is effectively bound by a quantifier or something that expands to one (such as "there exists at most one"). It is defined in terms of the not-free predicate df-nf 1441 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_ x A <-> A. y F/ x y e. A )
Theorem	nfci 2289*	Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x y e. A   =>    |- F/_ x A
Theorem	nfcii 2290*	Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( y e. A -> A. x y e. A )   =>    |- F/_ x A
Theorem	nfcr 2291*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_ x A -> F/ x y e. A )
Theorem	nfcrii 2292*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   =>    |- ( y e. A -> A. x y e. A )
Theorem	nfcri 2293*	Consequence of the not-free predicate. (Note that unlike nfcr 2291, this does not require y and A to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   =>    |- F/ x y e. A
Theorem	nfcd 2294*	Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ y ph   &    |- ( ph -> F/ x y e. A )   =>    |- ( ph -> F/_ x A )
Theorem	nfceqi 2295	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   =>    |- ( F/_ x A <-> F/_ x B )
Theorem	nfcxfr 2296	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   &    |- F/_ x B   =>    |- F/_ x A
Theorem	nfcxfrd 2297	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x A )
Theorem	nfceqdf 2298	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/ x ph   &    |- ( ph -> A = B )   =>    |- ( ph -> ( F/_ x A <-> F/_ x B ) )
Theorem	nfcv 2299*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A
Theorem	nfcvd 2300*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )