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	mpteq2dv 5201*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2ia 5202	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq2i 5203	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq12i 5204	An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)
Theorem	nfmpt 5205*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)
Theorem	nfmpt1 5206	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	cbvmptf 5207*	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.) (Revised by Thierry Arnoux, 9-Mar-2017.) Add disjoint variable condition to avoid ax-13 2370. See cbvmptfg 5208 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptfg 5208	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. Usage of this theorem is discouraged because it depends on ax-13 2370. See cbvmptf 5207 for a version with more disjoint variable conditions, but not requiring ax-13 2370. (Contributed by NM, 11-Sep-2011.) (Revised by Thierry Arnoux, 9-Mar-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmpt 5209*	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.) Add disjoint variable condition to avoid ax-13 2370. See cbvmptg 5210 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptg 5210*	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. Usage of this theorem is discouraged because it depends on ax-13 2370. See cbvmpt 5209 for a version with more disjoint variable conditions, but not requiring ax-13 2370. (Contributed by NM, 11-Sep-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptv 5211*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) Add disjoint variable condition to avoid auxiliary axioms . See cbvmptvg 5212 for a less restrictive version requiring more axioms. (Revised by GG, 17-Nov-2024.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptvg 5212*	Rule to change the bound variable in a maps-to function, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. See cbvmptv 5211 for a version with more disjoint variable conditions, but not requiring ax-13 2370. (Contributed by Mario Carneiro, 19-Feb-2013.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	mptv 5213*	Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
⊢ (𝑥 ∈ V ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦 = 𝐵}
2.1.26  Transitive classes
Syntax	wtr 5214	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr 𝐴
Definition	df-tr 5215	Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6083). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5216 (which is suggestive of the word "transitive"), dftr2c 5217, dftr3 5220, dftr4 5221, dftr5 5218, and (when 𝐴 is a set) unisuc 6413. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
Theorem	dftr2 5216*	An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. Using dftr2c 5217 instead may avoid dependences on ax-11 2158. (Contributed by NM, 24-Apr-1994.)
⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
Theorem	dftr2c 5217*	Variant of dftr2 5216 with commuted quantifiers, useful for shortening proofs and avoiding ax-11 2158. (Contributed by BTernaryTau, 28-Dec-2024.)
⊢ (Tr 𝐴 ↔ ∀𝑦∀𝑥((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
Theorem	dftr5 5218*	An alternate way of defining a transitive class. Definition 1.1 of [Schloeder] p. 1. (Contributed by NM, 20-Mar-2004.) Avoid ax-11 2158. (Revised by BTernaryTau, 28-Dec-2024.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴)
Theorem	dftr5OLD 5219*	Obsolete version of dftr5 5218 as of 28-Dec-2024. (Contributed by NM, 20-Mar-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴)
Theorem	dftr3 5220*	An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
Theorem	dftr4 5221	An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ 𝐴 ⊆ 𝒫 𝐴)
Theorem	treq 5222	Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Theorem	trel 5223	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 5224	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.)
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐴) → 𝐵 ∈ 𝐴))
Theorem	trss 5225	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 5226	The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.)
⊢ ((Tr 𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∩ 𝐵))
Theorem	tr0 5227	The empty set is transitive. (Contributed by NM, 16-Sep-1993.)
⊢ Tr ∅
Theorem	trv 5228	The universe is transitive. (Contributed by NM, 14-Sep-2003.)
⊢ Tr V
Theorem	triun 5229	An indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	truni 5230*	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 5231	An indexed intersection of a class of transitive sets is transitive. (Contributed by BJ, 3-Oct-2022.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∩ 𝑥 ∈ 𝐴 𝐵)
Theorem	trint 5232*	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 5233	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 5234*	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 6605). 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 5242, where you can find some further remarks. A slightly more compact version is shown as axrep2 5237. A quite different variant is zfrep6 7933, which if used in place of ax-rep 5234 would also require that the Separation Scheme axsep 5250 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 9844 and the Boundedness Axiom bnd 9845. Many developments of set theory distinguish the uses of Replacement from uses of the weaker axioms of Separation axsep 5250, Null Set axnul 5260, and Pairing axpr 5382, 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 5251, ax-nul 5261, and ax-pr 5387 below the theorems that prove them. (Contributed by NM, 23-Dec-1993.)
⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))
Theorem	axrep1 5235*	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 5234 → axrep1 5235 → axrep2 5237 → axrepnd 10547 → zfcndrep 10567 = ax-rep 5234. (Contributed by NM, 19-Nov-2005.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) Remove dependency on ax-13 2370. (Revised by BJ, 31-May-2019.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)))
Theorem	axreplem 5236*	Lemma for axrep2 5237 and axrep3 5238. (Contributed by BJ, 6-Aug-2022.)
⊢ (𝑥 = 𝑦 → (∃𝑢(𝜑 → ∀𝑣(𝜓 ↔ ∃𝑤(𝑧 ∈ 𝑥 ∧ 𝜒))) ↔ ∃𝑢(𝜑 → ∀𝑣(𝜓 ↔ ∃𝑤(𝑧 ∈ 𝑦 ∧ 𝜒)))))
Theorem	axrep2 5237*	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 2370. (Revised by BJ, 31-May-2019.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
Theorem	axrep3 5238*	Axiom of Replacement slightly strengthened from axrep2 5237; 𝑤 may occur free in 𝜑. (Contributed by NM, 2-Jan-1997.) Remove dependency on ax-13 2370. (Revised by BJ, 31-May-2019.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)))
Theorem	axrep4v 5239*	Version of axrep4 5240 with a disjoint variable condition, requiring fewer axioms. (Contributed by Matthew House, 18-Sep-2025.)
⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))
Theorem	axrep4 5240*	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 5241*	Obsolete version of axrep4 5240 as of 18-Sep-2025. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))
Theorem	axrep5 5242*	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 5243*	A condensed form of ax-rep 5234. (Contributed by SN, 18-Sep-2023.) (Proof shortened by Matthew House, 18-Sep-2025.)
⊢ (∀𝑤∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑))
Theorem	axrep6OLD 5244*	Obsolete version of axrep6 5243 as of 18-Sep-2025. (Contributed by SN, 18-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑤∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑))
Theorem	axrep6g 5245*	axrep6 5243 in class notation. It is equivalent to both ax-rep 5234 and abrexexg 7939, providing a direct link between the two. (Contributed by SN, 11-Dec-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥∃*𝑦𝜓) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜓} ∈ V)
Theorem	zfrepclf 5246*	An inference based on the Axiom of Replacement. Typically, 𝜑 defines a function from 𝑥 to 𝑦. (Contributed by NM, 26-Nov-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧))    ⇒   ⊢ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	zfrep3cl 5247*	An inference based on the Axiom of Replacement. Typically, 𝜑 defines a function from 𝑥 to 𝑦. (Contributed by NM, 26-Nov-1995.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧))    ⇒   ⊢ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	zfrep4 5248*	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 5249*	A more general version axsepg 5252 of the axiom scheme of separation ax-sep 5251 derived from the axiom scheme of replacement ax-rep 5234 (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 2119 to ax-13 2370. (Revised by SN, 25-Sep-2023.) Use ax-sep 5251 instead (or axsepg 5252 if the extra generality is needed). (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsep 5250*	Axiom scheme of separation ax-sep 5251 derived from the axiom scheme of replacement ax-rep 5234. The statement is identical to that of ax-sep 5251, and therefore shows that ax-sep 5251 is redundant when ax-rep 5234 is allowed. See ax-sep 5251 for more information. (Contributed by NM, 11-Sep-2006.) Use ax-sep 5251 instead. (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Axiom	ax-sep 5251*	Axiom scheme of separation. This is an axiom scheme of Zermelo and Zermelo-Fraenkel set theories. It was derived as axsep 5250 above and is therefore redundant in ZF set theory, which contains ax-rep 5234 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 3751. 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 5253, 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 5318 shows (showing the necessity of that condition in zfauscl 5253). Scheme Sep of [BellMachover] p. 463. (Contributed by NM, 11-Sep-2006.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg 5252*	A more general version of the axiom scheme of separation ax-sep 5251, 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 5251 with no additional set theory axioms. Note that it was also derived from ax-rep 5234 but without ax-sep 5251 as axsepgfromrep 5249. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) Remove dependency on ax-12 2178 and ax-13 2370 and shorten proof. (Revised by BJ, 6-Oct-2019.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	zfauscl 5253*	Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 5251, we invoke the Axiom of Extensionality (indirectly via vtocl 3524), 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 5318 shows. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	sepexlem 5254*	Lemma for sepex 5255. Use sepex 5255 instead. (Contributed by Matthew House, 19-Sep-2025.) (New usage is discouraged.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 ∈ 𝑦) → ∃𝑧∀𝑥(𝑥 ∈ 𝑧 ↔ 𝜑))
Theorem	sepex 5255*	Convert implication to equivalence within an existence statement using the Separation Scheme (Aussonderung) ax-sep 5251. Similar to Theorem 1.3(ii) of [BellMachover] p. 463. (Contributed by Matthew House, 19-Sep-2025.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 ∈ 𝑦) → ∃𝑧∀𝑥(𝑥 ∈ 𝑧 ↔ 𝜑))
Theorem	sepexi 5256*	Convert implication to equivalence within an existence statement using the Separation Scheme (Aussonderung) ax-sep 5251. Inference associated with sepex 5255. (Contributed by NM, 21-Jun-1993.) Generalize conclusion, extract closed form, and avoid ax-9 2119. (Revised by Matthew House, 19-Sep-2025.)
⊢ ∃𝑦∀𝑥(𝜑 → 𝑥 ∈ 𝑦)    ⇒   ⊢ ∃𝑧∀𝑥(𝑥 ∈ 𝑧 ↔ 𝜑)
Theorem	bm1.3iiOLD 5257*	Obsolete version of sepexi 5256 as of 18-Sep-2025. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥)    ⇒   ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)
Theorem	ax6vsep 5258*	Derive ax6v 1968 (a weakened version of ax-6 1967 where 𝑥 and 𝑦 must be distinct), from Separation ax-sep 5251 and Extensionality ax-ext 2701. See ax6 2382 for the derivation of ax-6 1967 from ax6v 1968. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2.2.3  Derive the Null Set Axiom
Theorem	axnulALT 5259*	Alternate proof of axnul 5260, proved from propositional calculus, ax-gen 1795, ax-4 1809, sp 2184, and ax-rep 5234. To check this, replace sp 2184 with the obsolete axiom ax-c5 38876 in the proof of axnulALT 5259 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 5260*	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 5251. 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 2706). This proof, suggested by Jeff Hoffman, uses only ax-4 1809 and ax-gen 1795 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 5251 implies the existence of at least one set. Note that Kunen's version of ax-sep 5251 (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 5259 for a proof directly from ax-rep 5234. This theorem should not be referenced by any proof. Instead, use ax-nul 5261 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 5261*	The Null Set Axiom of ZF set theory. It was derived as axnul 5260 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 5262	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 5261. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ∅ ∈ V
Theorem	al0ssb 5263*	The empty set is the unique class which is a subclass of any set. (Contributed by AV, 24-Aug-2022.)
⊢ (∀𝑦 𝑋 ⊆ 𝑦 ↔ 𝑋 = ∅)
Theorem	sseliALT 5264	Alternate proof of sseli 3942 illustrating the use of the weak deduction theorem to prove it from the inference sselii 3943. (Contributed by NM, 24-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
Theorem	csbexg 5265	The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 17-Aug-2018.)
⊢ (∀𝑥 𝐵 ∈ 𝑊 → ⦋𝐴 / 𝑥⦌𝐵 ∈ V)
Theorem	csbex 5266	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 5267	A version of unisn 4890 without the 𝐴 ∈ V hypothesis. (Contributed by Stefan Allan, 14-Mar-2006.)
⊢ ∪ {𝐴} ∈ {∅, 𝐴}
2.2.4  Theorems requiring subset and intersection existence
Theorem	nalset 5268*	No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) Remove use of ax-12 2178 and ax-13 2370. (Revised by BJ, 31-May-2019.)
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥
Theorem	vnex 5269	The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.)
⊢ ¬ ∃𝑥 𝑥 = V
Theorem	vprc 5270	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 5271	The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.)
⊢ ¬ V ∈ 𝐴
Theorem	inex1 5272	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∩ 𝐵) ∈ V
Theorem	inex2 5273	Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∩ 𝐴) ∈ V
Theorem	inex1g 5274	Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)
Theorem	inex2g 5275	Sufficient condition for an intersection to be a set. Commuted form of inex1g 5274. (Contributed by Peter Mazsa, 19-Dec-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∩ 𝐴) ∈ V)
Theorem	ssex 5276	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 5251 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
Theorem	ssexi 5277	The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 ∈ V
Theorem	ssexg 5278	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 5279	A subclass of a set is a set. Deduction form of ssexg 5278. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	abexd 5280*	Conditions for a class abstraction to be a set, deduction form. (Contributed by AV, 19-Apr-2025.)
⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ∈ V)
Theorem	abex 5281*	Conditions for a class abstraction to be a set. Remark: This proof is shorter than a proof using abexd 5280. (Contributed by AV, 19-Apr-2025.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∣ 𝜑} ∈ V
Theorem	prcssprc 5282	The superclass of a proper class is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∉ V) → 𝐵 ∉ V)
Theorem	sselpwd 5283	Elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)
Theorem	difexg 5284	Existence of a difference. (Contributed by NM, 26-May-1998.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)
Theorem	difexi 5285	Existence of a difference, inference version of difexg 5284. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Revised by AV, 26-Mar-2021.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∖ 𝐵) ∈ V
Theorem	difexd 5286	Existence of a difference. (Contributed by SN, 16-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ V)
Theorem	zfausab 5287*	Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V
Theorem	elpw2g 5288	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	elpw2 5289	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)
Theorem	elpwi2 5290	Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.)
⊢ 𝐵 ∈ 𝑉    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 ∈ 𝒫 𝐵
Theorem	rabelpw 5291*	A restricted class abstraction is an element of the power set of its restricting set. (Contributed by AV, 9-Oct-2023.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ 𝒫 𝐴)
Theorem	rabexg 5292*	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 5293*	Obsolete version of rabexg 5292 as of 24-Jul-2025). (Contributed by NM, 23-Oct-1999.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	rabex 5294*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V
Theorem	rabexd 5295*	Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5296. (Contributed by AV, 16-Jul-2019.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)
Theorem	rabex2 5296*	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 5297*	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 5298*	Membership in a class abstraction involving a subset. Unlike elabg 3643, 𝐴 does not have to be a set. (Contributed by NM, 29-Aug-2006.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝜑)} ↔ (𝐴 ⊆ 𝐵 ∧ 𝜓)))
Theorem	intex 5299	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 5300	If a class intersection is not a set, it must be the universe. (Contributed by NM, 3-Jul-2005.)
⊢ (¬ ∩ 𝐴 ∈ V ↔ ∩ 𝐴 = V)