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	mpteq1 5201*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mpteq1d 5202*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mpteq1i 5203	An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) Remove all disjoint variable conditions. (Revised by SN, 11-Nov-2024.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)
Theorem	mpteq2da 5204	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 5205*	Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) Remove dependency on ax-10 2176. (Revised by SN, 11-Nov-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2dv 5206*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2ia 5207	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq2i 5208	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq12i 5209	An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)
Theorem	nfmpt 5210*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)
Theorem	nfmpt1 5211	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	cbvmptf 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. (Contributed by NM, 11-Sep-2011.) (Revised by Thierry Arnoux, 9-Mar-2017.) Add disjoint variable condition to avoid ax-13 2404. See cbvmptfg 5213 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptfg 5213	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 2404. See cbvmptf 5212 for a version with more disjoint variable conditions, but not requiring ax-13 2404. (Contributed by NM, 11-Sep-2011.) (Revised by Thierry Arnoux, 9-Mar-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmpt 5214*	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 2404. See cbvmptg 5215 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptg 5215*	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 2404. See cbvmpt 5214 for a version with more disjoint variable conditions, but not requiring ax-13 2404. (Contributed by NM, 11-Sep-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptv 5216*	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 5217 for a less restrictive version requiring more axioms. (Revised by GG, 17-Nov-2024.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptvg 5217*	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 2404. See cbvmptv 5216 for a version with more disjoint variable conditions, but not requiring ax-13 2404. (Contributed by Mario Carneiro, 19-Feb-2013.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	mptv 5218*	Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
⊢ (𝑥 ∈ V ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦 = 𝐵}
2.1.26  Transitive classes
Syntax	wtr 5219	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr 𝐴
Definition	df-tr 5220	Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6114). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5221 (which is suggestive of the word "transitive"), dftr2c 5222, dftr3 5224, dftr4 5225, dftr5 5223, and (when 𝐴 is a set) unisuc 6444. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
Theorem	dftr2 5221*	An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. Using dftr2c 5222 instead may avoid dependences on ax-11 2192. (Contributed by NM, 24-Apr-1994.)
⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
Theorem	dftr2c 5222*	Variant of dftr2 5221 with commuted quantifiers, useful for shortening proofs and avoiding ax-11 2192. (Contributed by BTernaryTau, 28-Dec-2024.)
⊢ (Tr 𝐴 ↔ ∀𝑦∀𝑥((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
Theorem	dftr5 5223*	An alternate way of defining a transitive class. Definition 1.1 of [Schloeder] p. 1. (Contributed by NM, 20-Mar-2004.) Avoid ax-11 2192. (Revised by BTernaryTau, 28-Dec-2024.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴)
Theorem	dftr3 5224*	An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
Theorem	dftr4 5225	An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ 𝐴 ⊆ 𝒫 𝐴)
Theorem	treq 5226	Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Theorem	trel 5227	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 5228	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.)
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐴) → 𝐵 ∈ 𝐴))
Theorem	trss 5229	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	trun 5230	The union of transitive classes is transitive. (Contributed by Eric Schmidt, 19-Apr-2026.)
⊢ ((Tr 𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∪ 𝐵))
Theorem	trin 5231	The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.)
⊢ ((Tr 𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∩ 𝐵))
Theorem	tr0 5232	The empty set is transitive. (Contributed by NM, 16-Sep-1993.)
⊢ Tr ∅
Theorem	trv 5233	The universe is transitive. (Contributed by NM, 14-Sep-2003.)
⊢ Tr V
Theorem	triun 5234	An indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	truni 5235*	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 5236	An indexed intersection of a class of transitive sets is transitive. (Contributed by BJ, 3-Oct-2022.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∩ 𝑥 ∈ 𝐴 𝐵)
Theorem	trint 5237*	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 5238	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 5239*	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 6625). 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 5247, where you can find some further remarks. A slightly more compact version is shown as axrep2 5242. A quite different variant is zfrep6 5251, which if used in place of ax-rep 5239 would also require that the Separation Scheme axsep 5257 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 9878 and the Boundedness Axiom bnd 9879. Many developments of set theory distinguish the uses of Replacement from uses of the weaker axioms of Separation axsep 5257, Null Set axnul 5269, and Pairing axpr 5400, 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 5258, ax-nul 5270, and ax-pr 5406 below the theorems that prove them. (Contributed by NM, 23-Dec-1993.)
⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))
Theorem	axrep1 5240*	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 5239 → axrep1 5240 → axrep2 5242 → axrepnd 10580 → zfcndrep 10600 = ax-rep 5239. (Contributed by NM, 19-Nov-2005.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) Remove dependency on ax-13 2404. (Revised by BJ, 31-May-2019.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)))
Theorem	axreplem 5241*	Lemma for axrep2 5242 and axrep3 5243. (Contributed by BJ, 6-Aug-2022.)
⊢ (𝑥 = 𝑦 → (∃𝑢(𝜑 → ∀𝑣(𝜓 ↔ ∃𝑤(𝑧 ∈ 𝑥 ∧ 𝜒))) ↔ ∃𝑢(𝜑 → ∀𝑣(𝜓 ↔ ∃𝑤(𝑧 ∈ 𝑦 ∧ 𝜒)))))
Theorem	axrep2 5242*	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 2404. (Revised by BJ, 31-May-2019.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
Theorem	axrep3 5243*	Axiom of Replacement slightly strengthened from axrep2 5242; 𝑤 may occur free in 𝜑. (Contributed by NM, 2-Jan-1997.) Remove dependency on ax-13 2404. (Revised by BJ, 31-May-2019.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)))
Theorem	axrep4v 5244*	Version of axrep4 5245 with a disjoint variable condition, requiring fewer axioms. (Contributed by Matthew House, 18-Sep-2025.)
⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))
Theorem	axrep4 5245*	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 5246*	Obsolete version of axrep4 5245 as of 18-Sep-2025. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))
Theorem	axrep5 5247*	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 5248*	A condensed form of ax-rep 5239. (Contributed by SN, 18-Sep-2023.) (Proof shortened by Matthew House, 18-Sep-2025.)
⊢ (∀𝑤∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑))
Theorem	axrep6OLD 5249*	Obsolete version of axrep6 5248 as of 18-Sep-2025. (Contributed by SN, 18-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑤∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑))
Theorem	replem 5250*	A lemma for variants of the axiom of replacement: if we can form the set of images of the functional relation, then we can also form a set containing all its images. The converse requires the axiom of separation. (Contributed by BJ, 5-Apr-2026.)
⊢ ((∀𝑥 ∈ 𝑧 ∃𝑦𝜑 ∧ ∃𝑤∀𝑦(𝑦 ∈ 𝑤 ↔ ∃𝑥 ∈ 𝑧 𝜑)) → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑)
Theorem	zfrep6 5251*	A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 5258 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 in place of our ax-rep 5239. (Contributed by NM, 10-Oct-2003.) Shorten proof and reduce axiom dependencies. (Revised by BJ, 5-Apr-2026.)
⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑)
Theorem	axrep6g 5252*	axrep6 5248 in class notation. It is equivalent to both ax-rep 5239 and abrexexg 7959, providing a direct link between the two. (Contributed by SN, 11-Dec-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥∃*𝑦𝜓) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜓} ∈ V)
Theorem	zfrepclf 5253*	An inference based on the Axiom of Replacement. Typically, 𝜑 defines a function from 𝑥 to 𝑦. (Contributed by NM, 26-Nov-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧))    ⇒   ⊢ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	zfrep3cl 5254*	An inference based on the Axiom of Replacement. Typically, 𝜑 defines a function from 𝑥 to 𝑦. (Contributed by NM, 26-Nov-1995.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧))    ⇒   ⊢ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	zfrep4 5255*	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 5256*	A more general version axsepg 5259 of the axiom scheme of separation ax-sep 5258 derived from the axiom scheme of replacement ax-rep 5239 (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 2153 to ax-13 2404. (Revised by SN, 25-Sep-2023.) Use ax-sep 5258 instead (or axsepg 5259 if the extra generality is needed). (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsep 5257*	Axiom scheme of separation ax-sep 5258 derived from the axiom scheme of replacement ax-rep 5239. The statement is identical to that of ax-sep 5258, and therefore shows that ax-sep 5258 is redundant when ax-rep 5239 is allowed. See ax-sep 5258 for more information. (Contributed by NM, 11-Sep-2006.) Use ax-sep 5258 instead. (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Axiom	ax-sep 5258*	Axiom scheme of separation. This is an axiom scheme of Zermelo and Zermelo-Fraenkel set theories. It was derived as axsep 5257 above and is therefore redundant in ZF set theory, which contains ax-rep 5239 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 3744. 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 sepg 5260, 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 notsep 5336 shows (showing the necessity of that condition in sepgi 5261, hence in sepg 5260 and ax-sep 5258). Scheme Sep of [BellMachover] p. 463. (Contributed by NM, 11-Sep-2006.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg 5259*	A more general version of the axiom scheme of separation ax-sep 5258, 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 5258 with no additional set theory axioms. Note that it was also derived from ax-rep 5239 but without ax-sep 5258 as axsepgfromrep 5256. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) Remove dependency on ax-12 2213 and ax-13 2404 and shorten proof. (Revised by BJ, 6-Oct-2019.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	sepg 5260*	Version of the axiom of separation where the "containing set" is a class variable and the sethood assumption is in the antecedent. (Contributed by NM, 21-Jun-1993.) Put sepgi 5261 in closed form. (Revised by BJ, 2-Jul-2022.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
Theorem	sepgi 5261*	Inference associated with sepg 5260. The requirement that 𝑦 not occur in 𝜑 is necessary, as notsep 5336 shows. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 14-Jul-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	zfausclOLD 5262*	Obsolete version of sepgi 5261 as of 14-Jul-2026. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	sepexlem 5263*	Lemma for sepex 5264. Use sepex 5264 instead. (Contributed by Matthew House, 19-Sep-2025.) (New usage is discouraged.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 ∈ 𝑦) → ∃𝑧∀𝑥(𝑥 ∈ 𝑧 ↔ 𝜑))
Theorem	sepex 5264*	Convert implication to equivalence within an existence statement using the Separation Scheme (Aussonderung) ax-sep 5258. Similar to Theorem 1.3(ii) of [BellMachover] p. 463. (Contributed by Matthew House, 19-Sep-2025.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 ∈ 𝑦) → ∃𝑧∀𝑥(𝑥 ∈ 𝑧 ↔ 𝜑))
Theorem	sepexi 5265*	Convert implication to equivalence within an existence statement using the Separation Scheme (Aussonderung) ax-sep 5258. Inference associated with sepex 5264. (Contributed by NM, 21-Jun-1993.) Generalize conclusion, extract closed form, and avoid ax-9 2153. (Revised by Matthew House, 19-Sep-2025.)
⊢ ∃𝑦∀𝑥(𝜑 → 𝑥 ∈ 𝑦)    ⇒   ⊢ ∃𝑧∀𝑥(𝑥 ∈ 𝑧 ↔ 𝜑)
Theorem	bm1.3iiOLD 5266*	Obsolete version of sepexi 5265 as of 18-Sep-2025. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥)    ⇒   ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)
Theorem	ax6vsep 5267*	Derive ax6v 1998 (a weakened version of ax-6 1997 where 𝑥 and 𝑦 must be distinct), from Separation ax-sep 5258 and Extensionality ax-ext 2735. See ax6 2416 for the derivation of ax-6 1997 from ax6v 1998. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2.2.3  Derive the Null Set Axiom
Theorem	axnulALT 5268*	Alternate proof of axnul 5269, proved from propositional calculus, ax-gen 1825, ax-4 1839, sp 2219, and ax-rep 5239. To check this, replace sp 2219 with the obsolete axiom ax-c5 39635 in the proof of axnulALT 5268 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 5269*	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 5258. 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 2740). This proof, suggested by Jeff Hoffman, uses only ax-4 1839 and ax-gen 1825 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 5258 implies the existence of at least one set. Note that Kunen's version of ax-sep 5258 (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 5268 for a proof directly from ax-rep 5239. This theorem should not be referenced by any proof. Instead, use ax-nul 5270 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 5270*	The Null Set Axiom of ZF set theory. It was derived as axnul 5269 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 5271	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 5270. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ∅ ∈ V
Theorem	al0ssb 5272*	The empty set is the unique class which is a subclass of any set. (Contributed by AV, 24-Aug-2022.)
⊢ (∀𝑦 𝑋 ⊆ 𝑦 ↔ 𝑋 = ∅)
Theorem	sseliALT 5273	Alternate proof of sseli 3934 illustrating the use of the weak deduction theorem to prove it from the inference sselii 3935. (Contributed by NM, 24-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
Theorem	csbexg 5274	The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 17-Aug-2018.)
⊢ (∀𝑥 𝐵 ∈ 𝑊 → ⦋𝐴 / 𝑥⦌𝐵 ∈ V)
Theorem	csbex 5275	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 5276	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	exnelv 5277*	For any set 𝑥, there is a set not contained in 𝑥. The proof is based on Russell's paradox. (Contributed by NM, 23-Aug-1993.) Remove use of ax-12 2213 and ax-13 2404. (Revised by BJ, 31-May-2019.) Extract from nalset 5278. (Revised by Matthew House, 12-Apr-2026.)
⊢ ∃𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	nalset 5278*	No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) Extract exnelv 5277. (Revised by Matthew House, 12-Apr-2026.)
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥
Theorem	nalsetOLD 5279*	Obsolete version of nalset 5278 as of 12-Apr-2026. (Contributed by NM, 23-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥
Theorem	vneqv 5280	The universal class is not equal to any setvar. (Contributed by NM, 4-Jul-2005.) Extract from vnex 5281 and shorten proof. (Revised by BJ, 25-Apr-2026.)
⊢ ¬ 𝑥 = V
Theorem	vnex 5281	The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.) (Proof shortened by BJ, 25-Apr-2026.)
⊢ ¬ ∃𝑥 𝑥 = V
Theorem	vnexOLD 5282	Obsolete proof of vnex 5281 as of 25-Apr-2026. (Contributed by NM, 4-Jul-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∃𝑥 𝑥 = V
Theorem	nvel 5283	The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.) Prove it without using vprc 5284, which is then proved as an instance of it. (Revised by BJ, 1-May-2026.)
⊢ ¬ V ∈ 𝐴
Theorem	vprc 5284	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.) (Proof shortened by BJ, 1-May-2026.)
⊢ ¬ V ∈ V
Theorem	vprcOLD 5285	Obsolete proof of vprc 5284, obsolete as of 1-May-2026. (Contributed by NM, 23-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ V ∈ V
Theorem	nvelOLD 5286	Obsolete proof of nvel 5283, obsolete as of 1-May-2026. (Contributed by FL, 31-Dec-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ V ∈ 𝐴
Theorem	inex1 5287	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∩ 𝐵) ∈ V
Theorem	inex2 5288	Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∩ 𝐴) ∈ V
Theorem	inex1g 5289	Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)
Theorem	inex2g 5290	Sufficient condition for an intersection to be a set. Commuted form of inex1g 5289. (Contributed by Peter Mazsa, 19-Dec-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∩ 𝐴) ∈ V)
Theorem	ssexg 5291	A subclass of a set is a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) (Proof shortened by BJ, 18-Jul-2026.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	ssex 5292	A subclass of a set is a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 5258 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) (Proof shortened by BJ, 18-Jul-2026.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
Theorem	ssexOLD 5293	Obsolete version of ssex 5292 as of 18-Jul-2026. (Contributed by NM, 27-Apr-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
Theorem	ssexi 5294	A subclass of a set is a set. (Contributed by NM, 9-Sep-1993.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 ∈ V
Theorem	ssexgOLD 5295	Obsolete version of ssexg 5291 as of 18-Jul-2026. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	ssexd 5296	A subclass of a set is a set. Deduction form of ssexg 5291. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	abexd 5297*	Conditions for a class abstraction to be a set, deduction form. (Contributed by AV, 19-Apr-2025.)
⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ∈ V)
Theorem	abex 5298*	Conditions for a class abstraction to be a set. Remark: This proof is shorter than a proof using abexd 5297. (Contributed by AV, 19-Apr-2025.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∣ 𝜑} ∈ V
Theorem	prcssprc 5299	The superclass of a proper class is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∉ V) → 𝐵 ∉ V)
Theorem	sselpwd 5300	Membership in a power set. (Contributed by Thierry Arnoux, 18-May-2020.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)