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	eleq2w 2201	Weaker version of eleq2 2203 (but more general than elequ2 1691) not depending on ax-ext 2121 nor df-cleq 2132. (Contributed by BJ, 29-Sep-2019.)
|- ( x = y -> ( A e. x <-> A e. y ) )
Theorem	eleq1 2202	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( A e. C <-> B e. C ) )
Theorem	eleq2 2203	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( C e. A <-> C e. B ) )
Theorem	eleq12 2204	Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
|- ( ( A = B /\ C = D ) -> ( A e. C <-> B e. D ) )
Theorem	eleq1i 2205	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( A e. C <-> B e. C )
Theorem	eleq2i 2206	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>    |- ( C e. A <-> C e. B )
Theorem	eleq12i 2207	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 2208	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 2209	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 2210	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 2211	A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
|- ( A e. B -> ( C = A -> C e. B ) )
Theorem	eqeltri 2212	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B e. C   =>    |- A e. C
Theorem	eqeltrri 2213	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- A e. C   =>    |- B e. C
Theorem	eleqtri 2214	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- B = C   =>    |- A e. C
Theorem	eleqtrri 2215	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- C = B   =>    |- A e. C
Theorem	eqeltrd 2216	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 2217	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 2218	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 2219	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 2220	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 2221	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 2222	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 2223	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 2224	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 2225	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 2226	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A = B   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	eqeltrrid 2227	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- B = A   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	eleqtrid 2228	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> B = C )   =>    |- ( ph -> A e. C )
Theorem	eleqtrrid 2229	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> C = B )   =>    |- ( ph -> A e. C )
Theorem	eqeltrdi 2230	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A = B )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	eqeltrrdi 2231	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> B = A )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	eleqtrdi 2232	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A e. B )   &    |- B = C   =>    |- ( ph -> A e. C )
Theorem	eleqtrrdi 2233	A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
|- ( ph -> A e. B )   &    |- C = B   =>    |- ( ph -> A e. C )
Theorem	eleq2s 2234	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 2235	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 2236	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 2237	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 2238	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 2239*	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2305. (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 2240	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 2241	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 2242*	Lemma for eqsb3 2243. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( [ y / x ] x = A <-> y = A )
Theorem	eqsb3 2243*	Substitution applied to an atomic wff (class version of equsb3 1924). (Contributed by Rodolfo Medina, 28-Apr-2010.)
|- ( [ y / x ] x = A <-> y = A )
Theorem	clelsb3 2244*	Substitution applied to an atomic wff (class version of elsb3 1951). (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 2245*	Substitution applied to an atomic wff (class version of elsb4 1952). (Contributed by Jim Kingdon, 22-Nov-2018.)
|- ( [ y / x ] A e. x <-> A e. y )
Theorem	hbxfreq 2246	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1448 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 2247*	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 2248*	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 2253 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 2249*	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 2250	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 2251	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 2252	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 2253	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 2254*	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 2255	Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   =>    |- { x | ph } = { x | ps }
Theorem	abbid 2256	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 2257*	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 2258*	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 2259*	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 2260*	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 2261	Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.)
|- F/ y ph   =>    |- { x | ph } = { y | [ y / x ] ph }
Theorem	cbvabw 2262*	Version of cbvab 2263 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
Theorem	cbvab 2263	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 2264*	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 2265*	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 2266*	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 2267*	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 2268	Extend wff definition to include the not-free predicate for classes.
wff F/_ x A
Theorem	nfcjust 2269*	Justification theorem for df-nfc 2270. (Contributed by Mario Carneiro, 13-Oct-2016.)
|- ( A. y F/ x y e. A <-> A. z F/ x z e. A )
Definition	df-nfc 2270*	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 1437 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 2271*	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 2272*	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 2273*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_ x A -> F/ x y e. A )
Theorem	nfcrii 2274*	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 2275*	Consequence of the not-free predicate. (Note that unlike nfcr 2273, 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 2276*	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 2277	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   =>    |- ( F/_ x A <-> F/_ x B )
Theorem	nfcxfr 2278	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 2279	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 2280	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 2281*	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 2282*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )
Theorem	nfab1 2283	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x { x | ph }
Theorem	nfnfc1 2284	x is bound in F/_ x A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/_ x A
Theorem	clelsb3f 2285	Substitution applied to an atomic wff (class version of elsb3 1951). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.)
|- F/_ x A   =>    |- ( [ y / x ] x e. A <-> y e. A )
Theorem	nfab 2286	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/_ x { y | ph }
Theorem	nfaba1 2287	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_ x { y | A. x ph }
Theorem	nfnfc 2288	Hypothesis builder for F/_ y A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   =>    |- F/ x F/_ y A
Theorem	nfeq 2289	Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A = B
Theorem	nfel 2290	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A e. B
Theorem	nfeq1 2291*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A = B
Theorem	nfel1 2292*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A e. B
Theorem	nfeq2 2293*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A = B
Theorem	nfel2 2294*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A e. B
Theorem	nfcrd 2295*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/ x y e. A )
Theorem	nfeqd 2296	Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A = B )
Theorem	nfeld 2297	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A e. B )
Theorem	drnfc1 2298	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- ( A. x x = y -> A = B )   =>    |- ( A. x x = y -> ( F/_ x A <-> F/_ y B ) )
Theorem	drnfc2 2299	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- ( A. x x = y -> A = B )   =>    |- ( A. x x = y -> ( F/_ z A <-> F/_ z B ) )
Theorem	nfabd 2300	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/_ x { y | ps } )