P. 43 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4201-4300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfopab1 4201	The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x { <. x , y >. | ph }
Theorem	nfopab2 4202	The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ y { <. x , y >. | ph }
Theorem	cbvopab 4203*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
|- F/ z ph   &    |- F/ w ph   &    |- F/ x ps   &    |- F/ y ps   &    |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , w >. | ps }
Theorem	cbvopabv 4204*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , w >. | ps }
Theorem	cbvopab1 4205*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/ z ph   &    |- F/ x ps   &    |- ( x = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , y >. | ps }
Theorem	cbvopab2 4206*	Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
|- F/ z ph   &    |- F/ y ps   &    |- ( y = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. x , z >. | ps }
Theorem	cbvopab1s 4207*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
|- { <. x , y >. | ph } = { <. z , y >. | [ z / x ] ph }
Theorem	cbvopab1v 4208*	Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|- ( x = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , y >. | ps }
Theorem	cbvopab2v 4209*	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
|- ( y = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. x , z >. | ps }
Theorem	csbopabg 4210*	Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- ( A e. V -> [_ A / x ]_ { <. y , z >. | ph } = { <. y , z >. | [. A / x ]. ph } )
Theorem	unopab 4211	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
|- ( { <. x , y >. | ph } u. { <. x , y >. | ps } ) = { <. x , y >. | ( ph \/ ps ) }
Theorem	mpteq12f 4212	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12dva 4213*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> A = C )   &    |- ( ( ph /\ x e. A ) -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12dv 4214*	An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12 4215*	An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.)
|- ( ( A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq1 4216*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ( A = B -> ( x e. A |-> C ) = ( x e. B |-> C ) )
Theorem	mpteq1d 4217*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> ( x e. A |-> C ) = ( x e. B |-> C ) )
Theorem	mpteq1i 4218	An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) Remove all disjoint variable conditions. (Revised by SN, 11-Nov-2024.)
|- A = B   =>    |- ( x e. A |-> C ) = ( x e. B |-> C )
Theorem	mpteq2ia 4219	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ( x e. A -> B = C )   =>    |- ( x e. A |-> B ) = ( x e. A |-> C )
Theorem	mpteq2i 4220	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- B = C   =>    |- ( x e. A |-> B ) = ( x e. A |-> C )
Theorem	mpteq12i 4221	An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- A = C   &    |- B = D   =>    |- ( x e. A |-> B ) = ( x e. C |-> D )
Theorem	mpteq2da 4222	Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )
Theorem	mpteq2dva 4223*	Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )
Theorem	mpteq2dv 4224*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> B = C )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )
Theorem	nfmpt 4225*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( y e. A |-> B )
Theorem	nfmpt1 4226	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
|- F/_ x ( x e. A |-> B )
Theorem	cbvmptf 4227*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Thierry Arnoux, 9-Mar-2017.)
|- F/_ x A   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- ( x e. A |-> B ) = ( y e. A |-> C )
Theorem	cbvmpt 4228*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
|- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- ( x e. A |-> B ) = ( y e. A |-> C )
Theorem	cbvmptv 4229*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
|- ( x = y -> B = C )   =>    |- ( x e. A |-> B ) = ( y e. A |-> C )
Theorem	mptv 4230*	Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
|- ( x e. _V |-> B ) = { <. x , y >. | y = B }
2.1.24  Transitive classes
Syntax	wtr 4231	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr A
Definition	df-tr 4232	Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4233 (which is suggestive of the word "transitive"), dftr3 4235, dftr4 4236, and dftr5 4234. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.)
|- ( Tr A <-> U. A C_ A )
Theorem	dftr2 4233*	An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.)
|- ( Tr A <-> A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) )
Theorem	dftr5 4234*	An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.)
|- ( Tr A <-> A. x e. A A. y e. x y e. A )
Theorem	dftr3 4235*	An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.)
|- ( Tr A <-> A. x e. A x C_ A )
Theorem	dftr4 4236	An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.)
|- ( Tr A <-> A C_ ~P A )
Theorem	treq 4237	Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
|- ( A = B -> ( Tr A <-> Tr B ) )
Theorem	trel 4238	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( Tr A -> ( ( B e. C /\ C e. A ) -> B e. A ) )
Theorem	trel3 4239	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.)
|- ( Tr A -> ( ( B e. C /\ C e. D /\ D e. A ) -> B e. A ) )
Theorem	trss 4240	An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.)
|- ( Tr A -> ( B e. A -> B C_ A ) )
Theorem	trin 4241	The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.)
|- ( ( Tr A /\ Tr B ) -> Tr ( A i^i B ) )
Theorem	tr0 4242	The empty set is transitive. (Contributed by NM, 16-Sep-1993.)
|- Tr (/)
Theorem	trv 4243	The universe is transitive. (Contributed by NM, 14-Sep-2003.)
|- Tr _V
Theorem	triun 4244*	The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( A. x e. A Tr B -> Tr U_ x e. A B )
Theorem	truni 4245*	The union of a class of transitive sets is transitive. Exercise 5(a) of [Enderton] p. 73. (Contributed by Scott Fenton, 21-Feb-2011.) (Proof shortened by Mario Carneiro, 26-Apr-2014.)
|- ( A. x e. A Tr x -> Tr U. A )
Theorem	trint 4246*	The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. (Contributed by Scott Fenton, 25-Feb-2011.)
|- ( A. x e. A Tr x -> Tr |^| A )
Theorem	trintssm 4247*	Any inhabited transitive class includes its intersection. Similar to Exercise 3 in [TakeutiZaring] p. 44 (which mistakenly does not include the inhabitedness hypothesis). (Contributed by Jim Kingdon, 22-Aug-2018.)
|- ( ( Tr A /\ E. x x e. A ) -> |^| A C_ A )
2.2  IZF Set Theory - add the Axioms of Collection and Separation
2.2.1  Introduce the Axiom of Collection
Axiom	ax-coll 4248*	Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 4311 but uses a freeness hypothesis in place of one of the distinct variable conditions. (Contributed by Jim Kingdon, 23-Aug-2018.)
|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
Theorem	repizf 4249*	Axiom of Replacement. Axiom 7' of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). In our context this is not an axiom, but a theorem proved from ax-coll 4248. It is identical to zfrep6 4250 except for the choice of a freeness hypothesis rather than a disjoint variable condition between b and ph. (Contributed by Jim Kingdon, 23-Aug-2018.)
|- F/ b ph   =>    |- ( A. x e. a E! y ph -> E. b A. x e. a E. y e. b ph )
Theorem	zfrep6 4250*	A version of the Axiom of Replacement. Normally ph would have free variables x and y. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4251 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version. (Contributed by NM, 10-Oct-2003.)
|- ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )
2.2.2  Introduce the Axiom of Separation
Axiom	ax-sep 4251*	The Axiom of Separation of IZF set theory. Axiom 6 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed, and with a F/ y ph condition replaced by a disjoint variable condition between y and ph). The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with x e. z) so that it asserts the existence of a collection only if it is smaller than some other collection z that already exists. This prevents Russell's paradox ru 3050. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. The variable x can occur in the formula ph, which in textbooks is often written ph ( x ). To specify this in the Metamath language, we omit the distinct variable condition ($d) that x not occur in ph. For a version using a class variable, see sepg 4253, which requires the axiom of extensionality as well as the axiom scheme of separation for its derivation. If we omit the requirement that y not occur in ph, we can derive a contradiction (the ax-sep in set.mm). (Contributed by NM, 11-Sep-2006.)
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
Theorem	axsepg 4252*	A less restrictive version of the Separation Scheme ax-sep 4251, where variables x and z can both appear free in the wff ph, which can therefore be thought of as ph ( x , z ). This version was derived from the more restrictive ax-sep 4251 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
Theorem	sepg 4253*	Version of the axiom of separation where the "containing set" is a class variable and the sethood assumption is in the antecedent. (Contributed by NM, 21-Jun-1993.) Put sepgi 4254 in closed form. (Revised by BJ, 2-Jul-2022.)
|- ( A e. V -> E. y A. x ( x e. y <-> ( x e. A /\ ph ) ) )
Theorem	sepgi 4254*	Inference associated with sepg 4253. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 14-Jul-2026.)
|- A e. _V   =>    |- E. y A. x ( x e. y <-> ( x e. A /\ ph ) )
Theorem	zfausclOLD 4255*	Obsolete version of sepgi 4254 as of 14-Jul-2026. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- A e. _V   =>    |- E. y A. x ( x e. y <-> ( x e. A /\ ph ) )
Theorem	bm1.3ii 4256*	Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4251. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.)
|- E. x A. y ( ph -> y e. x )   =>    |- E. x A. y ( y e. x <-> ph )
Theorem	a9evsep 4257*	Derive a weakened version of ax-i9 1583, where x and y must be distinct, from Separation ax-sep 4251 and Extensionality ax-ext 2220. The theorem -. A. x -. x = y also holds (ax9vsep 4258), but in intuitionistic logic E. x x = y is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- E. x x = y
Theorem	ax9vsep 4258*	Derive a weakened version of ax-9 1584, where x and y must be distinct, from Separation ax-sep 4251 and Extensionality ax-ext 2220. In intuitionistic logic a9evsep 4257 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
|- -. A. x -. x = y
2.2.3  Derive the Null Set Axiom
Theorem	zfnuleu 4259*	Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2223 to strengthen the hypothesis in the form of axnul 4260). (Contributed by NM, 22-Dec-2007.)
|- E. x A. y -. y e. x   =>    |- E! x A. y -. y e. x
Theorem	axnul 4260*	The Null Set Axiom of ZF set theory: there exists a set with no elements. Axiom of Empty Set of [Enderton] p. 18. In some textbooks, this is presented as a separate axiom; here we show it can be derived from Separation ax-sep 4251. This version of the Null Set Axiom tells us that at least one empty set exists, but does not tell us that it is unique - we need the Axiom of Extensionality to do that (see zfnuleu 4259). This theorem should not be referenced by any proof. Instead, use ax-nul 4261 below so that the uses of the Null Set Axiom can be more easily identified. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Revised by NM, 4-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- E. x A. y -. y e. x
Axiom	ax-nul 4261*	The Null Set Axiom of IZF set theory. It was derived as axnul 4260 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. Axiom 4 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by NM, 7-Aug-2003.)
|- E. x A. y -. y e. x
Theorem	0ex 4262	The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 4261. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- (/) e. _V
Theorem	csbexga 4263	The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- ( ( A e. V /\ A. x B e. W ) -> [_ A / x ]_ B e. _V )
Theorem	csbexa 4264	The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- A e. _V   &    |- B e. _V   =>    |- [_ A / x ]_ B e. _V
2.2.4  Theorems requiring subset and intersection existence
Theorem	nalset 4265*	No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.)
|- -. E. x A. y y e. x
Theorem	vnex 4266	The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.)
|- -. E. x x = _V
Theorem	vprc 4267	The universal class is not a member of itself (and thus is not a set). Proposition 5.21 of [TakeutiZaring] p. 21; our proof, however, does not depend on the Axiom of Regularity. (Contributed by NM, 23-Aug-1993.)
|- -. _V e. _V
Theorem	nvel 4268	The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.)
|- -. _V e. A
Theorem	inex1 4269	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   =>    |- ( A i^i B ) e. _V
Theorem	inex2 4270	Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
|- A e. _V   =>    |- ( B i^i A ) e. _V
Theorem	inex1g 4271	Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
|- ( A e. V -> ( A i^i B ) e. _V )
Theorem	ssex 4272	The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 4251 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
|- B e. _V   =>    |- ( A C_ B -> A e. _V )
Theorem	ssexi 4273	The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)
|- B e. _V   &    |- A C_ B   =>    |- A e. _V
Theorem	ssexg 4274	The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.)
|- ( ( A C_ B /\ B e. C ) -> A e. _V )
Theorem	ssexd 4275	A subclass of a set is a set. Deduction form of ssexg 4274. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> B e. C )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> A e. _V )
Theorem	prcssprc 4276	The superclass of a proper class is a proper class. (Contributed by AV, 27-Dec-2020.)
|- ( ( A C_ B /\ A e/ _V ) -> B e/ _V )
Theorem	difexg 4277	Existence of a difference. (Contributed by NM, 26-May-1998.)
|- ( A e. V -> ( A \ B ) e. _V )
Theorem	difexi 4278	Existence of a difference, inference version of difexg 4277. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Revised by AV, 26-Mar-2021.)
|- A e. _V   =>    |- ( A \ B ) e. _V
Theorem	difexd 4279	Existence of a difference. (Contributed by SN, 16-Jul-2024.)
|- ( ph -> A e. V )   =>    |- ( ph -> ( A \ B ) e. _V )
Theorem	sepab 4280*	Separation Scheme (Aussonderung) in terms of a class abstraction. Prefer using the more natural statement rabexg 4281. (Contributed by NM, 8-Jun-1994.) Put in closed form. (Revised by BJ, 18-Jul-2026.)
|- ( A e. V -> { x | ( x e. A /\ ph ) } e. _V )
Theorem	rabexg 4281*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.)
|- ( A e. V -> { x e. A | ph } e. _V )
Theorem	rabex 4282*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
|- A e. _V   =>    |- { x e. A | ph } e. _V
Theorem	rabexd 4283*	Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 4284. (Contributed by AV, 16-Jul-2019.)
|- B = { x e. A | ps }   &    |- ( ph -> A e. V )   =>    |- ( ph -> B e. _V )
Theorem	rabex2 4284*	Separation Scheme in terms of a restricted class abstraction. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.)
|- B = { x e. A | ps }   &    |- A e. _V   =>    |- B e. _V
Theorem	rab2ex 4285*	A class abstraction based on a class abstraction based on a set is a set. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.)
|- B = { y e. A | ps }   &    |- A e. _V   =>    |- { x e. B | ph } e. _V
Theorem	elssabg 4286*	Membership in a class abstraction involving a subset. Unlike elabg 2972, A does not have to be a set. (Contributed by NM, 29-Aug-2006.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( B e. V -> ( A e. { x | ( x C_ B /\ ph ) } <-> ( A C_ B /\ ps ) ) )
Theorem	inteximm 4287*	The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
|- ( E. x x e. A -> |^| A e. _V )
Theorem	intexr 4288	If the intersection of a class exists, the class is nonempty. (Contributed by Jim Kingdon, 27-Aug-2018.)
|- ( |^| A e. _V -> A =/= (/) )
Theorem	intnexr 4289	If a class intersection is the universe, it is not a set. In classical logic this would be an equivalence. (Contributed by Jim Kingdon, 27-Aug-2018.)
|- ( |^| A = _V -> -. |^| A e. _V )
Theorem	intexabim 4290	The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
|- ( E. x ph -> |^| { x | ph } e. _V )
Theorem	intexrabim 4291	The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
|- ( E. x e. A ph -> |^| { x e. A | ph } e. _V )
Theorem	iinexgm 4292*	The existence of an indexed union. x is normally a free-variable parameter in B, which should be read B ( x ). (Contributed by Jim Kingdon, 28-Aug-2018.)
|- ( ( E. x x e. A /\ A. x e. A B e. C ) -> |^|_ x e. A B e. _V )
Theorem	inuni 4293*	The intersection of a union U. A with a class B is equal to the union of the intersections of each element of A with B. (Contributed by FL, 24-Mar-2007.)
|- ( U. A i^i B ) = U. { x | E. y e. A x = ( y i^i B ) }
Theorem	elpw2g 4294	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
|- ( B e. V -> ( A e. ~P B <-> A C_ B ) )
Theorem	elpw2 4295	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
|- B e. _V   =>    |- ( A e. ~P B <-> A C_ B )
Theorem	elpwi2 4296	Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.)
|- B e. V   &    |- A C_ B   =>    |- A e. ~P B
Theorem	if0elpw 4297	A conditional class with the False alternative being sent to the empty class is an element of the powerset of the class corresponding to the True alternative when that class is a set. This statement requires fewer axioms than the general case ifelpwung 4629. (Contributed by BJ, 5-May-2026.)
|- ( A e. V -> if ( ph , A , (/) ) e. ~P A )
Theorem	pwnss 4298	The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( A e. V -> -. ~P A C_ A )
Theorem	pwne 4299	No set equals its power set. The sethood antecedent is necessary; compare pwv 3934. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- ( A e. V -> ~P A =/= A )
Theorem	repizf2lem 4300	Lemma for repizf2 4301. If we have a function-like proposition which provides at most one value of y for each x in a set w, we can change "at most one" to "exactly one" by restricting the values of x to those values for which the proposition provides a value of y. (Contributed by Jim Kingdon, 7-Sep-2018.)
|- ( A. x e. w E* y ph <-> A. x e. { x e. w | E. y ph } E! y ph )