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	mpteq2dv 4201*	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 4202*	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 4203	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
|- F/_ x ( x e. A |-> B )
Theorem	cbvmptf 4204*	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 4205*	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 4206*	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 4207*	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 4208	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr A
Definition	df-tr 4209	Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4210 (which is suggestive of the word "transitive"), dftr3 4212, dftr4 4213, and dftr5 4211. 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 4210*	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 4211*	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 4212*	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 4213	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 4214	Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
|- ( A = B -> ( Tr A <-> Tr B ) )
Theorem	trel 4215	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 4216	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 4217	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 4218	The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.)
|- ( ( Tr A /\ Tr B ) -> Tr ( A i^i B ) )
Theorem	tr0 4219	The empty set is transitive. (Contributed by NM, 16-Sep-1993.)
|- Tr (/)
Theorem	trv 4220	The universe is transitive. (Contributed by NM, 14-Sep-2003.)
|- Tr _V
Theorem	triun 4221*	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 4222*	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 4223*	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 4224*	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 4225*	Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 4285 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 4226*	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 4225. It is identical to zfrep6 4227 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 4227*	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 4228 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 4228*	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 3041. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.)
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
Theorem	axsep2 4229*	A less restrictive version of the Separation Scheme ax-sep 4228, 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 4228 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	zfauscl 4230*	Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4228, we invoke the Axiom of Extensionality (indirectly via vtocl 2869), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   =>    |- E. y A. x ( x e. y <-> ( x e. A /\ ph ) )
Theorem	bm1.3ii 4231*	Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4228. 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 4232*	Derive a weakened version of ax-i9 1579, where x and y must be distinct, from Separation ax-sep 4228 and Extensionality ax-ext 2214. The theorem -. A. x -. x = y also holds (ax9vsep 4233), 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 4233*	Derive a weakened version of ax-9 1580, where x and y must be distinct, from Separation ax-sep 4228 and Extensionality ax-ext 2214. In intuitionistic logic a9evsep 4232 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 4234*	Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2217 to strengthen the hypothesis in the form of axnul 4235). (Contributed by NM, 22-Dec-2007.)
|- E. x A. y -. y e. x   =>    |- E! x A. y -. y e. x
Theorem	axnul 4235*	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 4228. 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 4234). This theorem should not be referenced by any proof. Instead, use ax-nul 4236 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 4236*	The Null Set Axiom of IZF set theory. It was derived as axnul 4235 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 4237	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 4236. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- (/) e. _V
Theorem	csbexga 4238	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 4239	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 4240*	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 4241	The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.)
|- -. E. x x = _V
Theorem	vprc 4242	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 4243	The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.)
|- -. _V e. A
Theorem	inex1 4244	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 4245	Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
|- A e. _V   =>    |- ( B i^i A ) e. _V
Theorem	inex1g 4246	Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
|- ( A e. V -> ( A i^i B ) e. _V )
Theorem	ssex 4247	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 4228 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
|- B e. _V   =>    |- ( A C_ B -> A e. _V )
Theorem	ssexi 4248	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 4249	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 4250	A subclass of a set is a set. Deduction form of ssexg 4249. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> B e. C )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> A e. _V )
Theorem	prcssprc 4251	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 4252	Existence of a difference. (Contributed by NM, 26-May-1998.)
|- ( A e. V -> ( A \ B ) e. _V )
Theorem	difexi 4253	Existence of a difference, inference version of difexg 4252. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Revised by AV, 26-Mar-2021.)
|- A e. _V   =>    |- ( A \ B ) e. _V
Theorem	zfausab 4254*	Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.)
|- A e. _V   =>    |- { x | ( x e. A /\ ph ) } e. _V
Theorem	rabexg 4255*	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 4256*	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 4257*	Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 4258. (Contributed by AV, 16-Jul-2019.)
|- B = { x e. A | ps }   &    |- ( ph -> A e. V )   =>    |- ( ph -> B e. _V )
Theorem	rabex2 4258*	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 4259*	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 4260*	Membership in a class abstraction involving a subset. Unlike elabg 2963, 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 4261*	The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
|- ( E. x x e. A -> |^| A e. _V )
Theorem	intexr 4262	If the intersection of a class exists, the class is nonempty. (Contributed by Jim Kingdon, 27-Aug-2018.)
|- ( |^| A e. _V -> A =/= (/) )
Theorem	intnexr 4263	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 4264	The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
|- ( E. x ph -> |^| { x | ph } e. _V )
Theorem	intexrabim 4265	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 4266*	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 4267*	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 4268	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 4269	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 4270	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 4271	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 4602. (Contributed by BJ, 5-May-2026.)
|- ( A e. V -> if ( ph , A , (/) ) e. ~P A )
Theorem	pwnss 4272	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 4273	No set equals its power set. The sethood antecedent is necessary; compare pwv 3913. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- ( A e. V -> ~P A =/= A )
Theorem	repizf2lem 4274	Lemma for repizf2 4275. 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 )
Theorem	repizf2 4275*	Replacement. This version of replacement is stronger than repizf 4226 in the sense that ph does not need to map all values of x in w to a value of y. The resulting set contains those elements for which there is a value of y and in that sense, this theorem combines repizf 4226 with ax-sep 4228. Another variation would be A. x e. w E* y ph -> { y | E. x ( x e. w /\ ph ) } e. _V but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.)
|- F/ z ph   =>    |- ( A. x e. w E* y ph -> E. z A. x e. { x e. w | E. y ph } E. y e. z ph )
2.2.5  Theorems requiring empty set existence
Theorem	class2seteq 4276*	Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.)
|- ( A e. V -> { x e. A | A e. _V } = A )
Theorem	0elpw 4277	Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
|- (/) e. ~P A
Theorem	0nep0 4278	The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.)
|- (/) =/= { (/) }
Theorem	0inp0 4279	Something cannot be equal to both the null set and the power set of the null set. (Contributed by NM, 30-Sep-2003.)
|- ( A = (/) -> -. A = { (/) } )
Theorem	unidif0 4280	The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.)
|- U. ( A \ { (/) } ) = U. A
Theorem	iin0imm 4281*	An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.)
|- ( E. y y e. A -> |^|_ x e. A (/) = (/) )
Theorem	iin0r 4282*	If an indexed intersection of the empty set is empty, the index set is nonempty. (Contributed by Jim Kingdon, 29-Aug-2018.)
|- ( |^|_ x e. A (/) = (/) -> A =/= (/) )
Theorem	intv 4283	The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.)
|- |^| _V = (/)
Theorem	axpweq 4284*	Two equivalent ways to express the Power Set Axiom. Note that ax-pow 4287 is not used by the proof. (Contributed by NM, 22-Jun-2009.)
|- A e. _V   =>    |- ( ~P A e. _V <-> E. x A. y ( A. z ( z e. y -> z e. A ) -> y e. x ) )
2.2.6  Collection principle
Theorem	bnd 4285*	A very strong generalization of the Axiom of Replacement (compare zfrep6 4227). Its strength lies in the rather profound fact that ph ( x , y ) does not have to be a "function-like" wff, as it does in the standard Axiom of Replacement. This theorem is sometimes called the Boundedness Axiom. In the context of IZF, it is just a slight variation of ax-coll 4225. (Contributed by NM, 17-Oct-2004.)
|- ( A. x e. z E. y ph -> E. w A. x e. z E. y e. w ph )
Theorem	bnd2 4286*	A variant of the Boundedness Axiom bnd 4285 that picks a subset z out of a possibly proper class B in which a property is true. (Contributed by NM, 4-Feb-2004.)
|- A e. _V   =>    |- ( A. x e. A E. y e. B ph -> E. z ( z C_ B /\ A. x e. A E. y e. z ph ) )
2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
2.3.1  Introduce the Axiom of Power Sets
Axiom	ax-pow 4287*	Axiom of Power Sets. An axiom of Intuitionistic Zermelo-Fraenkel set theory. It states that a set y exists that includes the power set of a given set x i.e. contains every subset of x. This is Axiom 8 of [Crosilla] p. "Axioms of CZF and IZF" except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 4231). The variant axpow2 4289 uses explicit subset notation. A version using class notation is pwex 4296. (Contributed by NM, 5-Aug-1993.)
|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
Theorem	zfpow 4288*	Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
|- E. x A. y ( A. x ( x e. y -> x e. z ) -> y e. x )
Theorem	axpow2 4289*	A variant of the Axiom of Power Sets ax-pow 4287 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
|- E. y A. z ( z C_ x -> z e. y )
Theorem	axpow3 4290*	A variant of the Axiom of Power Sets ax-pow 4287. For any set x, there exists a set y whose members are exactly the subsets of x i.e. the power set of x. Axiom Pow of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
|- E. y A. z ( z C_ x <-> z e. y )
Theorem	el 4291*	Every set is an element of some other set. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- E. y x e. y
Theorem	vpwex 4292	Power set axiom: the powerclass of a set is a set. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove pwexg 4293 from vpwex 4292. (Revised by BJ, 10-Aug-2022.)
|- ~P x e. _V
Theorem	pwexg 4293	Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003.)
|- ( A e. V -> ~P A e. _V )
Theorem	pwexd 4294	Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   =>    |- ( ph -> ~P A e. _V )
Theorem	abssexg 4295*	Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A e. V -> { x | ( x C_ A /\ ph ) } e. _V )
Theorem	pwex 4296	Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993.)
|- A e. _V   =>    |- ~P A e. _V
Theorem	snexg 4297	A singleton whose element exists is a set. The A e. _V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.)
|- ( A e. V -> { A } e. _V )
Theorem	snex 4298	A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
|- A e. _V   =>    |- { A } e. _V
Theorem	snexprc 4299	A singleton whose element is a proper class is a set. The -. A e. _V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.)
|- ( -. A e. _V -> { A } e. _V )
Theorem	notnotsnex 4300	A singleton is never a proper class. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jul-2022.)
|- -. -. { A } e. _V