P. 43 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4201-4300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zfrep6 4201*	A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4202 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 4202*	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 disjoint variable condition 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 3027. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsep2 4203*	A less restrictive version of the Separation Scheme ax-sep 4202, 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 4202 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	zfauscl 4204*	Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4202, we invoke the Axiom of Extensionality (indirectly via vtocl 2855), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	bm1.3ii 4205*	Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4202. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.)
⊢ ∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥)    ⇒   ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)
Theorem	a9evsep 4206*	Derive a weakened version of ax-i9 1576, where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 4202 and Extensionality ax-ext 2211. The theorem ¬ ∀𝑥¬ 𝑥 = 𝑦 also holds (ax9vsep 4207), but in intuitionistic logic ∃𝑥𝑥 = 𝑦 is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥 𝑥 = 𝑦
Theorem	ax9vsep 4207*	Derive a weakened version of ax-9 1577, where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 4202 and Extensionality ax-ext 2211. In intuitionistic logic a9evsep 4206 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 4208*	Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2214 to strengthen the hypothesis in the form of axnul 4209). (Contributed by NM, 22-Dec-2007.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥    ⇒   ⊢ ∃!𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	axnul 4209*	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 4202. 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 4208). This theorem should not be referenced by any proof. Instead, use ax-nul 4210 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 4210*	The Null Set Axiom of IZF set theory. It was derived as axnul 4209 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 4211	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 4210. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ∅ ∈ V
Theorem	csbexga 4212	The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 𝐵 ∈ 𝑊) → ⦋𝐴 / 𝑥⦌𝐵 ∈ V)
Theorem	csbexa 4213	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 4214*	No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.)
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥
Theorem	vnex 4215	The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.)
⊢ ¬ ∃𝑥 𝑥 = V
Theorem	vprc 4216	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 4217	The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.)
⊢ ¬ V ∈ 𝐴
Theorem	inex1 4218	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∩ 𝐵) ∈ V
Theorem	inex2 4219	Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∩ 𝐴) ∈ V
Theorem	inex1g 4220	Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)
Theorem	ssex 4221	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 4202 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
Theorem	ssexi 4222	The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 ∈ V
Theorem	ssexg 4223	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 4224	A subclass of a set is a set. Deduction form of ssexg 4223. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	difexg 4225	Existence of a difference. (Contributed by NM, 26-May-1998.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)
Theorem	zfausab 4226*	Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V
Theorem	rabexg 4227*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	rabex 4228*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V
Theorem	rabexd 4229*	Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 4230. (Contributed by AV, 16-Jul-2019.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)
Theorem	rabex2 4230*	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 4231*	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 4232*	Membership in a class abstraction involving a subset. Unlike elabg 2949, 𝐴 does not have to be a set. (Contributed by NM, 29-Aug-2006.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝜑)} ↔ (𝐴 ⊆ 𝐵 ∧ 𝜓)))
Theorem	inteximm 4233*	The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V)
Theorem	intexr 4234	If the intersection of a class exists, the class is nonempty. (Contributed by Jim Kingdon, 27-Aug-2018.)
⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
Theorem	intnexr 4235	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 4236	The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
⊢ (∃𝑥𝜑 → ∩ {𝑥 ∣ 𝜑} ∈ V)
Theorem	intexrabim 4237	The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∩ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	iinexgm 4238*	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 4239*	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 4240	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	elpw2 4241	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)
Theorem	elpwi2 4242	Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.)
⊢ 𝐵 ∈ 𝑉    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 ∈ 𝒫 𝐵
Theorem	pwnss 4243	The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝐴 ∈ 𝑉 → ¬ 𝒫 𝐴 ⊆ 𝐴)
Theorem	pwne 4244	No set equals its power set. The sethood antecedent is necessary; compare pwv 3887. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ≠ 𝐴)
Theorem	repizf2lem 4245	Lemma for repizf2 4246. 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 4246*	Replacement. This version of replacement is stronger than repizf 4200 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 4200 with ax-sep 4202. 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 4247*	Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V} = 𝐴)
Theorem	0elpw 4248	Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
⊢ ∅ ∈ 𝒫 𝐴
Theorem	0nep0 4249	The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.)
⊢ ∅ ≠ {∅}
Theorem	0inp0 4250	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 4251	The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.)
⊢ ∪ (𝐴 ∖ {∅}) = ∪ 𝐴
Theorem	iin0imm 4252*	An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.)
⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ∅ = ∅)
Theorem	iin0r 4253*	If an indexed intersection of the empty set is empty, the index set is nonempty. (Contributed by Jim Kingdon, 29-Aug-2018.)
⊢ (∩ 𝑥 ∈ 𝐴 ∅ = ∅ → 𝐴 ≠ ∅)
Theorem	intv 4254	The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.)
⊢ ∩ V = ∅
Theorem	axpweq 4255*	Two equivalent ways to express the Power Set Axiom. Note that ax-pow 4258 is not used by the proof. (Contributed by NM, 22-Jun-2009.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝒫 𝐴 ∈ V ↔ ∃𝑥∀𝑦(∀𝑧(𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝑥))
2.2.6  Collection principle
Theorem	bnd 4256*	A very strong generalization of the Axiom of Replacement (compare zfrep6 4201). Its strength lies in the rather profound fact that 𝜑(𝑥, 𝑦) does not have to be a "function-like" wff, as it does in the standard Axiom of Replacement. This theorem is sometimes called the Boundedness Axiom. In the context of IZF, it is just a slight variation of ax-coll 4199. (Contributed by NM, 17-Oct-2004.)
⊢ (∀𝑥 ∈ 𝑧 ∃𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑)
Theorem	bnd2 4257*	A variant of the Boundedness Axiom bnd 4256 that picks a subset 𝑧 out of a possibly proper class 𝐵 in which a property is true. (Contributed by NM, 4-Feb-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑧(𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑))
2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
2.3.1  Introduce the Axiom of Power Sets
Axiom	ax-pow 4258*	Axiom of Power Sets. An axiom of Intuitionistic Zermelo-Fraenkel set theory. It states that a set 𝑦 exists that includes the power set of a given set 𝑥 i.e. contains every subset of 𝑥. This is Axiom 8 of [Crosilla] p. "Axioms of CZF and IZF" except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 4205). The variant axpow2 4260 uses explicit subset notation. A version using class notation is pwex 4267. (Contributed by NM, 5-Aug-1993.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfpow 4259*	Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
⊢ ∃𝑥∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axpow2 4260*	A variant of the Axiom of Power Sets ax-pow 4258 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦)
Theorem	axpow3 4261*	A variant of the Axiom of Power Sets ax-pow 4258. For any set 𝑥, there exists a set 𝑦 whose members are exactly the subsets of 𝑥 i.e. the power set of 𝑥. Axiom Pow of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 ↔ 𝑧 ∈ 𝑦)
Theorem	el 4262*	Every set is an element of some other set. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	vpwex 4263	Power set axiom: the powerclass of a set is a set. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove pwexg 4264 from vpwex 4263. (Revised by BJ, 10-Aug-2022.)
⊢ 𝒫 𝑥 ∈ V
Theorem	pwexg 4264	Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
Theorem	pwexd 4265	Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ∈ V)
Theorem	abssexg 4266*	Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ∈ V)
Theorem	pwex 4267	Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝒫 𝐴 ∈ V
Theorem	snexg 4268	A singleton whose element exists is a set. The 𝐴 ∈ V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	snex 4269	A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ∈ V
Theorem	snexprc 4270	A singleton whose element is a proper class is a set. The ¬ 𝐴 ∈ V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.)
⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
Theorem	notnotsnex 4271	A singleton is never a proper class. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jul-2022.)
⊢ ¬ ¬ {𝐴} ∈ V
Theorem	p0ex 4272	The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.)
⊢ {∅} ∈ V
Theorem	pp0ex 4273	{∅, {∅}} (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.)
⊢ {∅, {∅}} ∈ V
Theorem	ord3ex 4274	The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.)
⊢ {∅, {∅}, {∅, {∅}}} ∈ V
Theorem	dtruarb 4275*	At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). This theorem asserts the existence of two sets which do not equal each other; compare with dtruex 4651 in which we are given a set 𝑦 and go from there to a set 𝑥 which is not equal to it. (Contributed by Jim Kingdon, 2-Sep-2018.)
⊢ ∃𝑥∃𝑦 ¬ 𝑥 = 𝑦
Theorem	pwuni 4276	A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.)
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
Theorem	undifexmid 4277*	Union of complementary parts producing the whole and excluded middle. Although special cases such as undifss 3572 and undifdcss 7093 are provable, the full statement implies excluded middle as shown here. (Contributed by Jim Kingdon, 16-Jun-2022.)
⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)    ⇒   ⊢ (𝜑 ∨ ¬ 𝜑)
2.3.2  A notation for excluded middle
Syntax	wem 4278	Formula for an abbreviation of excluded middle.
wff EXMID
Definition	df-exmid 4279	The expression EXMID will be used as a readable shorthand for any form of the law of the excluded middle; this is a useful shorthand largely because it hides statements of the form "for any proposition" in a system which can only quantify over sets, not propositions. To see how this compares with other ways of expressing excluded middle, compare undifexmid 4277 with exmidundif 4290. The former may be more recognizable as excluded middle because it is in terms of propositions, and the proof may be easier to follow for much the same reason (it just has to show 𝜑 and ¬ 𝜑 in the the relevant parts of the proof). The latter, however, has the key advantage of being able to prove both directions of the biconditional. To state that excluded middle implies a proposition is hard to do gracefully without EXMID, because there is no way to write a hypothesis 𝜑 ∨ ¬ 𝜑 for an arbitrary proposition; instead the hypothesis would need to be the particular instance of excluded middle which that proof needs. Or to say it another way, EXMID implies DECID 𝜑 by exmidexmid 4280 but there is no good way to express the converse. This definition and how we use it is easiest to understand (and most appropriate to assign the name "excluded middle" to) if we assume ax-sep 4202, in which case EXMID means that all propositions are decidable (see exmidexmid 4280 and notice that it relies on ax-sep 4202). If we instead work with ax-bdsep 16271, EXMID as defined here means that all bounded propositions are decidable. (Contributed by Mario Carneiro and Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥))
Theorem	exmidexmid 4280	EXMID implies that an arbitrary proposition is decidable. That is, EXMID captures the usual meaning of excluded middle when stated in terms of propositions. To get other propositional statements which are equivalent to excluded middle, combine this with notnotrdc 848, peircedc 919, or condc 858. (Contributed by Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID → DECID 𝜑)
Theorem	ss1o0el1 4281	A subclass of {∅} contains the empty set if and only if it equals {∅}. (Contributed by BJ and Jim Kingdon, 9-Aug-2024.)
⊢ (𝐴 ⊆ {∅} → (∅ ∈ 𝐴 ↔ 𝐴 = {∅}))
Theorem	exmid01 4282	Excluded middle is equivalent to saying any subset of {∅} is either ∅ or {∅}. (Contributed by BJ and Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅})))
Theorem	pwntru 4283	A slight strengthening of pwtrufal 16392. (Contributed by Mario Carneiro and Jim Kingdon, 12-Sep-2023.)
⊢ ((𝐴 ⊆ {∅} ∧ 𝐴 ≠ {∅}) → 𝐴 = ∅)
Theorem	exmid1dc 4284*	A convenience theorem for proving that something implies EXMID. Think of this as an alternative to using a proposition, as in proofs like undifexmid 4277 or ordtriexmid 4613. In this context 𝑥 = {∅} can be thought of as "x is true". (Contributed by Jim Kingdon, 21-Nov-2023.)
⊢ ((𝜑 ∧ 𝑥 ⊆ {∅}) → DECID 𝑥 = {∅})    ⇒   ⊢ (𝜑 → EXMID)
Theorem	exmidn0m 4285*	Excluded middle is equivalent to any set being empty or inhabited. (Contributed by Jim Kingdon, 5-Mar-2023.)
⊢ (EXMID ↔ ∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦 ∈ 𝑥))
Theorem	exmidsssn 4286*	Excluded middle is equivalent to the biconditionalized version of sssnr 3831 for sets. (Contributed by Jim Kingdon, 5-Mar-2023.)
⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ {𝑦} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑦})))
Theorem	exmidsssnc 4287*	Excluded middle in terms of subsets of a singleton. This is similar to exmid01 4282 but lets you choose any set as the element of the singleton rather than just ∅. It is similar to exmidsssn 4286 but for a particular set 𝐵 rather than all sets. (Contributed by Jim Kingdon, 29-Jul-2023.)
⊢ (𝐵 ∈ 𝑉 → (EXMID ↔ ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
Theorem	exmid0el 4288	Excluded middle is equivalent to decidability of ∅ being an element of an arbitrary set. (Contributed by Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥DECID ∅ ∈ 𝑥)
Theorem	exmidel 4289*	Excluded middle is equivalent to decidability of membership for two arbitrary sets. (Contributed by Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥∀𝑦DECID 𝑥 ∈ 𝑦)
Theorem	exmidundif 4290*	Excluded middle is equivalent to every subset having a complement. That is, the union of a subset and its relative complement being the whole set. Although special cases such as undifss 3572 and undifdcss 7093 are provable, the full statement is equivalent to excluded middle as shown here. (Contributed by Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
Theorem	exmidundifim 4291*	Excluded middle is equivalent to every subset having a complement. Variation of exmidundif 4290 with an implication rather than a biconditional. (Contributed by Jim Kingdon, 16-Feb-2023.)
⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
Theorem	exmid1stab 4292*	If every proposition is stable, excluded middle follows. We are thinking of 𝑥 as a proposition and 𝑥 = {∅} as "𝑥 is true". (Contributed by Jim Kingdon, 28-Nov-2023.)
⊢ ((𝜑 ∧ 𝑥 ⊆ {∅}) → STAB 𝑥 = {∅})    ⇒   ⊢ (𝜑 → EXMID)
2.3.3  Axiom of Pairing
Axiom	ax-pr 4293*	The Axiom of Pairing of IZF set theory. Axiom 2 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 4205). (Contributed by NM, 14-Nov-2006.)
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
Theorem	zfpair2 4294	Derive the abbreviated version of the Axiom of Pairing from ax-pr 4293. (Contributed by NM, 14-Nov-2006.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	prexg 4295	The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3777, prprc1 3775, and prprc2 3776. (Contributed by Jim Kingdon, 16-Sep-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
Theorem	snelpwg 4296	A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.) Put in closed form and avoid ax-nul 4210. (Revised by BJ, 17-Jan-2025.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵))
Theorem	snelpwi 4297	A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)
Theorem	snelpw 4298	A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵)
Theorem	prelpw 4299	An unordered pair of two sets is a member of the powerclass of a class if and only if the two sets are members of that class. (Contributed by AV, 8-Jan-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶))
Theorem	prelpwi 4300	A pair of two sets belongs to the power class of a class containing those two sets. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)