P. 41 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4001-4100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opabbid 4001	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})
Theorem	opabbidv 4002*	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})
Theorem	opabbii 4003	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Theorem	nfopab 4004*	Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧{⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	nfopab1 4005	The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	nfopab2 4006	The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	cbvopab 4007*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
Theorem	cbvopabv 4008*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
Theorem	cbvopab1 4009*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
Theorem	cbvopab2 4010*	Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
Theorem	cbvopab1s 4011*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ [𝑧 / 𝑥]𝜑}
Theorem	cbvopab1v 4012*	Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
Theorem	cbvopab2v 4013*	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
Theorem	csbopabg 4014*	Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑})
Theorem	unopab 4015	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ 𝜓)}
Theorem	mpteq12f 4016	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dva 4017*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dv 4018*	An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12 4019*	An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.)
⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq1 4020*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mpteq1d 4021*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mpteq2ia 4022	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq2i 4023	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq12i 4024	An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)
Theorem	mpteq2da 4025	Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2dva 4026*	Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2dv 4027*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	nfmpt 4028*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)
Theorem	nfmpt1 4029	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	cbvmptf 4030*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Thierry Arnoux, 9-Mar-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmpt 4031*	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.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptv 4032*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	mptv 4033*	Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
⊢ (𝑥 ∈ V ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦 = 𝐵}
2.1.24  Transitive classes
Syntax	wtr 4034	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr 𝐴
Definition	df-tr 4035	Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4036 (which is suggestive of the word "transitive"), dftr3 4038, dftr4 4039, and dftr5 4037. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
Theorem	dftr2 4036*	An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.)
⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
Theorem	dftr5 4037*	An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴)
Theorem	dftr3 4038*	An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
Theorem	dftr4 4039	An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ 𝐴 ⊆ 𝒫 𝐴)
Theorem	treq 4040	Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Theorem	trel 4041	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 4042	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.)
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐴) → 𝐵 ∈ 𝐴))
Theorem	trss 4043	An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.)
⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
Theorem	trin 4044	The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.)
⊢ ((Tr 𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∩ 𝐵))
Theorem	tr0 4045	The empty set is transitive. (Contributed by NM, 16-Sep-1993.)
⊢ Tr ∅
Theorem	trv 4046	The universe is transitive. (Contributed by NM, 14-Sep-2003.)
⊢ Tr V
Theorem	triun 4047*	The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	truni 4048*	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	trint 4049*	The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)
Theorem	trintssm 4050*	Any inhabited transitive class includes its intersection. Similar to Exercise 3 in [TakeutiZaring] p. 44 (which mistakenly does not include the inhabitedness hypothesis). (Contributed by Jim Kingdon, 22-Aug-2018.)
⊢ ((Tr 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ 𝐴)
2.2  IZF Set Theory - add the Axioms of Collection and Separation
2.2.1  Introduce the Axiom of Collection
Axiom	ax-coll 4051*	Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 4104 but uses a freeness hypothesis in place of one of the distinct variable constraints. (Contributed by Jim Kingdon, 23-Aug-2018.)
⊢ Ⅎ𝑏𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑)
Theorem	repizf 4052*	Axiom of Replacement. Axiom 7' of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). In our context this is not an axiom, but a theorem proved from ax-coll 4051. It is identical to zfrep6 4053 except for the choice of a freeness hypothesis rather than a distinct variable constraint between 𝑏 and 𝜑. (Contributed by Jim Kingdon, 23-Aug-2018.)
⊢ Ⅎ𝑏𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝑎 ∃!𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑)
Theorem	zfrep6 4053*	A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4054 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version. (Contributed by NM, 10-Oct-2003.)
⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑)
2.2.2  Introduce the Axiom of Separation
Axiom	ax-sep 4054*	The Axiom of Separation of IZF set theory. Axiom 6 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed, and with a Ⅎ𝑦𝜑 condition replaced by a distinct variable constraint between 𝑦 and 𝜑). The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with 𝑥 ∈ 𝑧) 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 2912. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsep2 4055*	A less restrictive version of the Separation Scheme ax-sep 4054, where variables 𝑥 and 𝑧 can both appear free in the wff 𝜑, which can therefore be thought of as 𝜑(𝑥, 𝑧). This version was derived from the more restrictive ax-sep 4054 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	zfauscl 4056*	Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4054, we invoke the Axiom of Extensionality (indirectly via vtocl 2743), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	bm1.3ii 4057*	Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4054. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.)
⊢ ∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥)    ⇒   ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)
Theorem	a9evsep 4058*	Derive a weakened version of ax-i9 1511, where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 4054 and Extensionality ax-ext 2122. The theorem ¬ ∀𝑥¬ 𝑥 = 𝑦 also holds (ax9vsep 4059), but in intuitionistic logic ∃𝑥𝑥 = 𝑦 is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥 𝑥 = 𝑦
Theorem	ax9vsep 4059*	Derive a weakened version of ax-9 1512, where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 4054 and Extensionality ax-ext 2122. In intuitionistic logic a9evsep 4058 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2.2.3  Derive the Null Set Axiom
Theorem	zfnuleu 4060*	Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2125 to strengthen the hypothesis in the form of axnul 4061). (Contributed by NM, 22-Dec-2007.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥    ⇒   ⊢ ∃!𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	axnul 4061*	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 4054. This version of the Null Set Axiom tells us that at least one empty set exists, but does not tell us that it is unique - we need the Axiom of Extensionality to do that (see zfnuleu 4060). This theorem should not be referenced by any proof. Instead, use ax-nul 4062 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 4062*	The Null Set Axiom of IZF set theory. It was derived as axnul 4061 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. Axiom 4 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by NM, 7-Aug-2003.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	0ex 4063	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 4062. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ∅ ∈ V
Theorem	csbexga 4064	The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 𝐵 ∈ 𝑊) → ⦋𝐴 / 𝑥⦌𝐵 ∈ V)
Theorem	csbexa 4065	The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V
2.2.4  Theorems requiring subset and intersection existence
Theorem	nalset 4066*	No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.)
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥
Theorem	vnex 4067	The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.)
⊢ ¬ ∃𝑥 𝑥 = V
Theorem	vprc 4068	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 4069	The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.)
⊢ ¬ V ∈ 𝐴
Theorem	inex1 4070	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∩ 𝐵) ∈ V
Theorem	inex2 4071	Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∩ 𝐴) ∈ V
Theorem	inex1g 4072	Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)
Theorem	ssex 4073	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 4054 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
Theorem	ssexi 4074	The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 ∈ V
Theorem	ssexg 4075	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 4076	A subclass of a set is a set. Deduction form of ssexg 4075. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	difexg 4077	Existence of a difference. (Contributed by NM, 26-May-1998.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)
Theorem	zfausab 4078*	Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V
Theorem	rabexg 4079*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	rabex 4080*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V
Theorem	elssabg 4081*	Membership in a class abstraction involving a subset. Unlike elabg 2834, 𝐴 does not have to be a set. (Contributed by NM, 29-Aug-2006.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝜑)} ↔ (𝐴 ⊆ 𝐵 ∧ 𝜓)))
Theorem	inteximm 4082*	The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
Theorem	intexr 4083	If the intersection of a class exists, the class is nonempty. (Contributed by Jim Kingdon, 27-Aug-2018.)
⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
Theorem	intnexr 4084	If a class intersection is the universe, it is not a set. In classical logic this would be an equivalence. (Contributed by Jim Kingdon, 27-Aug-2018.)
⊢ (∩ 𝐴 = V → ¬ ∩ 𝐴 ∈ V)
Theorem	intexabim 4085	The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
⊢ (∃𝑥𝜑 → ∩ {𝑥 ∣ 𝜑} ∈ V)
Theorem	intexrabim 4086	The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∩ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	iinexgm 4087*	The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵, which should be read 𝐵(𝑥). (Contributed by Jim Kingdon, 28-Aug-2018.)
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	inuni 4088*	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.)
⊢ (∪ 𝐴 ∩ 𝐵) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)}
Theorem	elpw2g 4089	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	elpw2 4090	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)
Theorem	pwnss 4091	The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝐴 ∈ 𝑉 → ¬ 𝒫 𝐴 ⊆ 𝐴)
Theorem	pwne 4092	No set equals its power set. The sethood antecedent is necessary; compare pwv 3743. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ≠ 𝐴)
Theorem	repizf2lem 4093	Lemma for repizf2 4094. If we have a function-like proposition which provides at most one value of 𝑦 for each 𝑥 in a set 𝑤, we can change "at most one" to "exactly one" by restricting the values of 𝑥 to those values for which the proposition provides a value of 𝑦. (Contributed by Jim Kingdon, 7-Sep-2018.)
⊢ (∀𝑥 ∈ 𝑤 ∃*𝑦𝜑 ↔ ∀𝑥 ∈ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑}∃!𝑦𝜑)
Theorem	repizf2 4094*	Replacement. This version of replacement is stronger than repizf 4052 in the sense that 𝜑 does not need to map all values of 𝑥 in 𝑤 to a value of 𝑦. The resulting set contains those elements for which there is a value of 𝑦 and in that sense, this theorem combines repizf 4052 with ax-sep 4054. Another variation would be ∀𝑥 ∈ 𝑤∃*𝑦𝜑 → {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)} ∈ V but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝑤 ∃*𝑦𝜑 → ∃𝑧∀𝑥 ∈ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑}∃𝑦 ∈ 𝑧 𝜑)
2.2.5  Theorems requiring empty set existence
Theorem	class2seteq 4095*	Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V} = 𝐴)
Theorem	0elpw 4096	Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
⊢ ∅ ∈ 𝒫 𝐴
Theorem	0nep0 4097	The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.)
⊢ ∅ ≠ {∅}
Theorem	0inp0 4098	Something cannot be equal to both the null set and the power set of the null set. (Contributed by NM, 30-Sep-2003.)
⊢ (𝐴 = ∅ → ¬ 𝐴 = {∅})
Theorem	unidif0 4099	The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.)
⊢ ∪ (𝐴 ∖ {∅}) = ∪ 𝐴
Theorem	iin0imm 4100*	An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.)
⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ∅ = ∅)