P. 53 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5201-5300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dftr2c 5201*	Variant of dftr2 5200 with commuted quantifiers, useful for shortening proofs and avoiding ax-11 2160. (Contributed by BTernaryTau, 28-Dec-2024.)
⊢ (Tr 𝐴 ↔ ∀𝑦∀𝑥((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
Theorem	dftr5 5202*	An alternate way of defining a transitive class. Definition 1.1 of [Schloeder] p. 1. (Contributed by NM, 20-Mar-2004.) Avoid ax-11 2160. (Revised by BTernaryTau, 28-Dec-2024.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴)
Theorem	dftr3 5203*	An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
Theorem	dftr4 5204	An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ 𝐴 ⊆ 𝒫 𝐴)
Theorem	treq 5205	Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Theorem	trel 5206	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴))
Theorem	trel3 5207	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.)
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐴) → 𝐵 ∈ 𝐴))
Theorem	trss 5208	An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
Theorem	trin 5209	The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.)
⊢ ((Tr 𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∩ 𝐵))
Theorem	tr0 5210	The empty set is transitive. (Contributed by NM, 16-Sep-1993.)
⊢ Tr ∅
Theorem	trv 5211	The universe is transitive. (Contributed by NM, 14-Sep-2003.)
⊢ Tr V
Theorem	triun 5212	An indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	truni 5213*	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.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴)
Theorem	triin 5214	An indexed intersection of a class of transitive sets is transitive. (Contributed by BJ, 3-Oct-2022.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∩ 𝑥 ∈ 𝐴 𝐵)
Theorem	trint 5215*	The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by BJ, 3-Oct-2022.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)
Theorem	trintss 5216	Any nonempty transitive class includes its intersection. Exercise 3 in [TakeutiZaring] p. 44 (which mistakenly does not include the nonemptiness hypothesis). (Contributed by Scott Fenton, 3-Mar-2011.) (Proof shortened by Andrew Salmon, 14-Nov-2011.)
⊢ ((Tr 𝐴 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ⊆ 𝐴)
2.2  ZF Set Theory - add the Axiom of Replacement
2.2.1  Introduce the Axiom of Replacement
Axiom	ax-rep 5217*	Axiom of Replacement. An axiom scheme of Zermelo-Fraenkel set theory. Axiom 5 of [TakeutiZaring] p. 19. It tells us that the image of any set under a function is also a set (see the variant funimaex 6569). Although 𝜑 may be any wff whatsoever, this axiom is useful (i.e. its antecedent is satisfied) when we are given some function and 𝜑 encodes the predicate "the value of the function at 𝑤 is 𝑧". Thus, 𝜑 will ordinarily have free variables 𝑤 and 𝑧- think of it informally as 𝜑(𝑤, 𝑧). We prefix 𝜑 with the quantifier ∀𝑦 in order to "protect" the axiom from any 𝜑 containing 𝑦, thus allowing us to eliminate any restrictions on 𝜑. Another common variant is derived as axrep5 5225, where you can find some further remarks. A slightly more compact version is shown as axrep2 5220. A quite different variant is zfrep6 7887, which if used in place of ax-rep 5217 would also require that the Separation Scheme axsep 5233 be stated as a separate axiom. There is a very strong generalization of Replacement that doesn't demand function-like behavior of 𝜑. Two versions of this generalization are called the Collection Principle cp 9781 and the Boundedness Axiom bnd 9782. Many developments of set theory distinguish the uses of Replacement from uses of the weaker axioms of Separation axsep 5233, Null Set axnul 5243, and Pairing axpr 5365, all of which we derive from Replacement. In order to make it easier to identify the uses of those redundant axioms, we restate them as Axioms ax-sep 5234, ax-nul 5244, and ax-pr 5370 below the theorems that prove them. (Contributed by NM, 23-Dec-1993.)
⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))
Theorem	axrep1 5218*	The version of the Axiom of Replacement used in the Metamath Solitaire applet https://us.metamath.org/mmsolitaire/mms.html. Equivalence is shown via the path ax-rep 5217 → axrep1 5218 → axrep2 5220 → axrepnd 10482 → zfcndrep 10502 = ax-rep 5217. (Contributed by NM, 19-Nov-2005.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) Remove dependency on ax-13 2372. (Revised by BJ, 31-May-2019.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)))
Theorem	axreplem 5219*	Lemma for axrep2 5220 and axrep3 5221. (Contributed by BJ, 6-Aug-2022.)
⊢ (𝑥 = 𝑦 → (∃𝑢(𝜑 → ∀𝑣(𝜓 ↔ ∃𝑤(𝑧 ∈ 𝑥 ∧ 𝜒))) ↔ ∃𝑢(𝜑 → ∀𝑣(𝜓 ↔ ∃𝑤(𝑧 ∈ 𝑦 ∧ 𝜒)))))
Theorem	axrep2 5220*	Axiom of Replacement expressed with the fewest number of different variables and without any restrictions on 𝜑. (Contributed by NM, 15-Aug-2003.) Remove dependency on ax-13 2372. (Revised by BJ, 31-May-2019.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
Theorem	axrep3 5221*	Axiom of Replacement slightly strengthened from axrep2 5220; 𝑤 may occur free in 𝜑. (Contributed by NM, 2-Jan-1997.) Remove dependency on ax-13 2372. (Revised by BJ, 31-May-2019.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)))
Theorem	axrep4v 5222*	Version of axrep4 5223 with a disjoint variable condition, requiring fewer axioms. (Contributed by Matthew House, 18-Sep-2025.)
⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))
Theorem	axrep4 5223*	A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Matthew House, 18-Sep-2025.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))
Theorem	axrep4OLD 5224*	Obsolete version of axrep4 5223 as of 18-Sep-2025. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))
Theorem	axrep5 5225*	Axiom of Replacement (similar to Axiom Rep of [BellMachover] p. 463). The antecedent tells us 𝜑 is analogous to a "function" from 𝑥 to 𝑦 (although it is not really a function since it is a wff and not a class). In the consequent we postulate the existence of a set 𝑧 that corresponds to the "image" of 𝜑 restricted to some other set 𝑤. The hypothesis says 𝑧 must not be free in 𝜑. (Contributed by NM, 26-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (∀𝑥(𝑥 ∈ 𝑤 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧)) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))
Theorem	axrep6 5226*	A condensed form of ax-rep 5217. (Contributed by SN, 18-Sep-2023.) (Proof shortened by Matthew House, 18-Sep-2025.)
⊢ (∀𝑤∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑))
Theorem	axrep6OLD 5227*	Obsolete version of axrep6 5226 as of 18-Sep-2025. (Contributed by SN, 18-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑤∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑))
Theorem	axrep6g 5228*	axrep6 5226 in class notation. It is equivalent to both ax-rep 5217 and abrexexg 7893, providing a direct link between the two. (Contributed by SN, 11-Dec-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥∃*𝑦𝜓) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜓} ∈ V)
Theorem	zfrepclf 5229*	An inference based on the Axiom of Replacement. Typically, 𝜑 defines a function from 𝑥 to 𝑦. (Contributed by NM, 26-Nov-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧))    ⇒   ⊢ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	zfrep3cl 5230*	An inference based on the Axiom of Replacement. Typically, 𝜑 defines a function from 𝑥 to 𝑦. (Contributed by NM, 26-Nov-1995.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧))    ⇒   ⊢ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	zfrep4 5231*	A version of Replacement using class abstractions. (Contributed by NM, 26-Nov-1995.)
⊢ {𝑥 ∣ 𝜑} ∈ V    &   ⊢ (𝜑 → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))    ⇒   ⊢ {𝑦 ∣ ∃𝑥(𝜑 ∧ 𝜓)} ∈ V
2.2.2  Derive the Axiom of Separation
Theorem	axsepgfromrep 5232*	A more general version axsepg 5235 of the axiom scheme of separation ax-sep 5234 derived from the axiom scheme of replacement ax-rep 5217 (and first-order logic). The extra generality consists in the absence of a disjoint variable condition on 𝑧, 𝜑 (that is, variable 𝑧 may occur in formula 𝜑). See linked statements for more information. (Contributed by NM, 11-Sep-2006.) Remove dependencies on ax-9 2121 to ax-13 2372. (Revised by SN, 25-Sep-2023.) Use ax-sep 5234 instead (or axsepg 5235 if the extra generality is needed). (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsep 5233*	Axiom scheme of separation ax-sep 5234 derived from the axiom scheme of replacement ax-rep 5217. The statement is identical to that of ax-sep 5234, and therefore shows that ax-sep 5234 is redundant when ax-rep 5217 is allowed. See ax-sep 5234 for more information. (Contributed by NM, 11-Sep-2006.) Use ax-sep 5234 instead. (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Axiom	ax-sep 5234*	Axiom scheme of separation. This is an axiom scheme of Zermelo and Zermelo-Fraenkel set theories. It was derived as axsep 5233 above and is therefore redundant in ZF set theory, which contains ax-rep 5217 as an axiom (contrary to Zermelo set theory). We state it as a separate axiom here so that some of its uses can be identified more easily. Some textbooks present the axiom scheme of separation as a separate axiom scheme in order to show that much of set theory can be derived without the stronger axiom scheme of replacement (which is not part of Zermelo set theory). The axiom scheme of separation is a weak form of Frege's axiom scheme of (unrestricted) comprehension, in that it conditions it with the condition 𝑥 ∈ 𝑧, so that it asserts the existence of a collection only if it is smaller than some other collection 𝑧 that already exists. This prevents Russell's paradox ru 3739. In some texts, this scheme is called "Aussonderung" (German for "separation") or "Subset Axiom". The variable 𝑥 can occur in the formula 𝜑, which in textbooks is often written 𝜑(𝑥). To specify this in the Metamath language, we omit the distinct variable condition ($d) that 𝑥 not occur in 𝜑. For a version using a class variable, see zfauscl 5236, which requires the axiom of extensionality as well as the axiom scheme of separation for its derivation. If we omit the requirement that 𝑦 not occur in 𝜑, we can derive a contradiction, as notzfaus 5301 shows (showing the necessity of that condition in zfauscl 5236). Scheme Sep of [BellMachover] p. 463. (Contributed by NM, 11-Sep-2006.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg 5235*	A more general version of the axiom scheme of separation ax-sep 5234, where variable 𝑧 can also occur (in addition to 𝑥) in formula 𝜑, which can therefore be thought of as 𝜑(𝑥, 𝑧). This version is derived from the more restrictive ax-sep 5234 with no additional set theory axioms. Note that it was also derived from ax-rep 5217 but without ax-sep 5234 as axsepgfromrep 5232. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) Remove dependency on ax-12 2180 and ax-13 2372 and shorten proof. (Revised by BJ, 6-Oct-2019.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	zfauscl 5236*	Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 5234, we invoke the Axiom of Extensionality (indirectly via vtocl 3513), which is needed for the justification of class variable notation. If we omit the requirement that 𝑦 not occur in 𝜑, we can derive a contradiction, as notzfaus 5301 shows. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	sepexlem 5237*	Lemma for sepex 5238. Use sepex 5238 instead. (Contributed by Matthew House, 19-Sep-2025.) (New usage is discouraged.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 ∈ 𝑦) → ∃𝑧∀𝑥(𝑥 ∈ 𝑧 ↔ 𝜑))
Theorem	sepex 5238*	Convert implication to equivalence within an existence statement using the Separation Scheme (Aussonderung) ax-sep 5234. Similar to Theorem 1.3(ii) of [BellMachover] p. 463. (Contributed by Matthew House, 19-Sep-2025.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 ∈ 𝑦) → ∃𝑧∀𝑥(𝑥 ∈ 𝑧 ↔ 𝜑))
Theorem	sepexi 5239*	Convert implication to equivalence within an existence statement using the Separation Scheme (Aussonderung) ax-sep 5234. Inference associated with sepex 5238. (Contributed by NM, 21-Jun-1993.) Generalize conclusion, extract closed form, and avoid ax-9 2121. (Revised by Matthew House, 19-Sep-2025.)
⊢ ∃𝑦∀𝑥(𝜑 → 𝑥 ∈ 𝑦)    ⇒   ⊢ ∃𝑧∀𝑥(𝑥 ∈ 𝑧 ↔ 𝜑)
Theorem	bm1.3iiOLD 5240*	Obsolete version of sepexi 5239 as of 18-Sep-2025. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥)    ⇒   ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)
Theorem	ax6vsep 5241*	Derive ax6v 1969 (a weakened version of ax-6 1968 where 𝑥 and 𝑦 must be distinct), from Separation ax-sep 5234 and Extensionality ax-ext 2703. See ax6 2384 for the derivation of ax-6 1968 from ax6v 1969. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2.2.3  Derive the Null Set Axiom
Theorem	axnulALT 5242*	Alternate proof of axnul 5243, proved from propositional calculus, ax-gen 1796, ax-4 1810, sp 2186, and ax-rep 5217. To check this, replace sp 2186 with the obsolete axiom ax-c5 38921 in the proof of axnulALT 5242 and type the Metamath program "MM> SHOW TRACE_BACK axnulALT / AXIOMS" command. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	axnul 5243*	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 5234. 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 nulmo 2708). This proof, suggested by Jeff Hoffman, uses only ax-4 1810 and ax-gen 1796 from predicate calculus, which are valid in "free logic" i.e. logic holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc] p. 277). Thus, our ax-sep 5234 implies the existence of at least one set. Note that Kunen's version of ax-sep 5234 (Axiom 3 of [Kunen] p. 11) does not imply the existence of a set because his is universally closed, i.e., prefixed with universal quantifiers to eliminate all free variables. His existence is provided by a separate axiom stating ∃𝑥𝑥 = 𝑥 (Axiom 0 of [Kunen] p. 10). See axnulALT 5242 for a proof directly from ax-rep 5217. This theorem should not be referenced by any proof. Instead, use ax-nul 5244 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.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Axiom	ax-nul 5244*	The Null Set Axiom of ZF set theory. It was derived as axnul 5243 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 7-Aug-2003.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	0ex 5245	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 5244. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ∅ ∈ V
Theorem	al0ssb 5246*	The empty set is the unique class which is a subclass of any set. (Contributed by AV, 24-Aug-2022.)
⊢ (∀𝑦 𝑋 ⊆ 𝑦 ↔ 𝑋 = ∅)
Theorem	sseliALT 5247	Alternate proof of sseli 3930 illustrating the use of the weak deduction theorem to prove it from the inference sselii 3931. (Contributed by NM, 24-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
Theorem	csbexg 5248	The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 17-Aug-2018.)
⊢ (∀𝑥 𝐵 ∈ 𝑊 → ⦋𝐴 / 𝑥⦌𝐵 ∈ V)
Theorem	csbex 5249	The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Revised by NM, 17-Aug-2018.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V
Theorem	unisn2 5250	A version of unisn 4878 without the 𝐴 ∈ V hypothesis. (Contributed by Stefan Allan, 14-Mar-2006.)
⊢ ∪ {𝐴} ∈ {∅, 𝐴}
2.2.4  Theorems requiring subset and intersection existence
Theorem	nalset 5251*	No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) Remove use of ax-12 2180 and ax-13 2372. (Revised by BJ, 31-May-2019.)
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥
Theorem	vnex 5252	The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.)
⊢ ¬ ∃𝑥 𝑥 = V
Theorem	vprc 5253	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 ∈ V
Theorem	nvel 5254	The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.)
⊢ ¬ V ∈ 𝐴
Theorem	inex1 5255	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∩ 𝐵) ∈ V
Theorem	inex2 5256	Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∩ 𝐴) ∈ V
Theorem	inex1g 5257	Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)
Theorem	inex2g 5258	Sufficient condition for an intersection to be a set. Commuted form of inex1g 5257. (Contributed by Peter Mazsa, 19-Dec-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∩ 𝐴) ∈ V)
Theorem	ssex 5259	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 5234 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
Theorem	ssexi 5260	The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 ∈ V
Theorem	ssexg 5261	The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	ssexd 5262	A subclass of a set is a set. Deduction form of ssexg 5261. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	abexd 5263*	Conditions for a class abstraction to be a set, deduction form. (Contributed by AV, 19-Apr-2025.)
⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ∈ V)
Theorem	abex 5264*	Conditions for a class abstraction to be a set. Remark: This proof is shorter than a proof using abexd 5263. (Contributed by AV, 19-Apr-2025.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∣ 𝜑} ∈ V
Theorem	prcssprc 5265	The superclass of a proper class is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∉ V) → 𝐵 ∉ V)
Theorem	sselpwd 5266	Elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)
Theorem	difexg 5267	Existence of a difference. (Contributed by NM, 26-May-1998.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)
Theorem	difexi 5268	Existence of a difference, inference version of difexg 5267. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Revised by AV, 26-Mar-2021.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∖ 𝐵) ∈ V
Theorem	difexd 5269	Existence of a difference. (Contributed by SN, 16-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ V)
Theorem	zfausab 5270*	Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V
Theorem	elpw2g 5271	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	elpw2 5272	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)
Theorem	elpwi2 5273	Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.)
⊢ 𝐵 ∈ 𝑉    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 ∈ 𝒫 𝐵
Theorem	rabelpw 5274*	A restricted class abstraction is an element of the power set of its restricting set. (Contributed by AV, 9-Oct-2023.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ 𝒫 𝐴)
Theorem	rabexg 5275*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) (Proof shortened by BJ, 24-Jul-2025.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	rabexgOLD 5276*	Obsolete version of rabexg 5275 as of 24-Jul-2025). (Contributed by NM, 23-Oct-1999.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	rabex 5277*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V
Theorem	rabexd 5278*	Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5279. (Contributed by AV, 16-Jul-2019.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)
Theorem	rabex2 5279*	Separation Scheme in terms of a restricted class abstraction. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐵 ∈ V
Theorem	rab2ex 5280*	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.)
⊢ 𝐵 = {𝑦 ∈ 𝐴 ∣ 𝜓}    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} ∈ V
Theorem	elssabg 5281*	Membership in a class abstraction involving a subset. Unlike elabg 3632, 𝐴 does not have to be a set. (Contributed by NM, 29-Aug-2006.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝜑)} ↔ (𝐴 ⊆ 𝐵 ∧ 𝜓)))
Theorem	intex 5282	The intersection of a nonempty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse. (Contributed by NM, 13-Aug-2002.)
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
Theorem	intnex 5283	If a class intersection is not a set, it must be the universe. (Contributed by NM, 3-Jul-2005.)
⊢ (¬ ∩ 𝐴 ∈ V ↔ ∩ 𝐴 = V)
Theorem	intexab 5284	The intersection of a nonempty class abstraction exists. (Contributed by NM, 21-Oct-2003.)
⊢ (∃𝑥𝜑 ↔ ∩ {𝑥 ∣ 𝜑} ∈ V)
Theorem	intexrab 5285	The intersection of a nonempty restricted class abstraction exists. (Contributed by NM, 21-Oct-2003.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∩ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	iinexg 5286*	The existence of a class intersection. 𝑥 is normally a free-variable parameter in 𝐵, which should be read 𝐵(𝑥). (Contributed by FL, 19-Sep-2011.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	intabs 5287*	Absorption of a redundant conjunct in the intersection of a class abstraction. (Contributed by NM, 3-Jul-2005.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = ∩ {𝑦 ∣ 𝜓} → (𝜑 ↔ 𝜒))    &   ⊢ (∩ {𝑦 ∣ 𝜓} ⊆ 𝐴 ∧ 𝜒)    ⇒   ⊢ ∩ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑}
Theorem	inuni 5288*	The intersection of a union ∪ 𝐴 with a class 𝐵 is equal to the union of the intersections of each element of 𝐴 with 𝐵. (Contributed by FL, 24-Mar-2007.) (Proof shortened by Wolf Lammen, 15-May-2025.)
⊢ (∪ 𝐴 ∩ 𝐵) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)}
Theorem	axpweq 5289*	Two equivalent ways to express the Power Set Axiom. Note that ax-pow 5303 is not used by the proof. When ax-pow 5303 is assumed and 𝐴 is a set, both sides of the biconditional hold. In ZF, both sides hold if and only if 𝐴 is a set (see pwexr 7698). (Contributed by NM, 22-Jun-2009.)
⊢ (𝒫 𝐴 ∈ V ↔ ∃𝑥∀𝑦(∀𝑧(𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝑥))
Theorem	pwnss 5290	The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Proof shortened by BJ, 24-Jul-2025.)
⊢ (𝐴 ∈ 𝑉 → ¬ 𝒫 𝐴 ⊆ 𝐴)
Theorem	pwne 5291	No set equals its power set. The sethood antecedent is necessary; compare pwv 4856. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ≠ 𝐴)
Theorem	difelpw 5292	A difference is an element of the power set of its minuend. (Contributed by AV, 9-Oct-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ 𝒫 𝐴)
2.2.5  Theorems requiring empty set existence
Theorem	class2set 5293*	The class of elements of 𝐴 "such that 𝐴 is a set" is a set. That class is equal to 𝐴 when 𝐴 is a set (see class2seteq 3663) and to the empty set when 𝐴 is a proper class. (Contributed by NM, 16-Oct-2003.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V} ∈ V
Theorem	0elpw 5294	Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
⊢ ∅ ∈ 𝒫 𝐴
Theorem	pwne0 5295	A power class is never empty. (Contributed by NM, 3-Sep-2018.)
⊢ 𝒫 𝐴 ≠ ∅
Theorem	0nep0 5296	The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.)
⊢ ∅ ≠ {∅}
Theorem	0inp0 5297	Something cannot be equal to both the null set and the power set of the null set. (Contributed by NM, 21-Jun-1993.)
⊢ (𝐴 = ∅ → ¬ 𝐴 = {∅})
Theorem	unidif0 5298	The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.)
⊢ ∪ (𝐴 ∖ {∅}) = ∪ 𝐴
Theorem	eqsnuniex 5299	If a class is equal to the singleton of its union, then its union exists. (Contributed by BTernaryTau, 24-Sep-2024.)
⊢ (𝐴 = {∪ 𝐴} → ∪ 𝐴 ∈ V)
Theorem	iin0 5300*	An indexed intersection of the empty set, with a nonempty index set, is empty. (Contributed by NM, 20-Oct-2005.)
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝑥 ∈ 𝐴 ∅ = ∅)