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