P. 41 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 4001-4100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfiin2g 4001*	Alternate definition of indexed intersection when B is a set. (Contributed by Jeff Hankins, 27-Aug-2009.)
⊢ (∀x ∈ A B ∈ C → ∩x ∈ A B = ∩{y ∣ ∃x ∈ A y = B})
Theorem	dfiun2 4002*	Alternate definition of indexed union when B is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ B ∈ V    ⇒   ⊢ ∪x ∈ A B = ∪{y ∣ ∃x ∈ A y = B}
Theorem	dfiin2 4003*	Alternate definition of indexed intersection when B is a set. Definition 15(b) of [Suppes] p. 44. (Contributed by NM, 28-Jun-1998.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ B ∈ V    ⇒   ⊢ ∩x ∈ A B = ∩{y ∣ ∃x ∈ A y = B}
Theorem	cbviun 4004*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.)
⊢ ℲyB    &   ⊢ ℲxC    &   ⊢ (x = y → B = C)    ⇒   ⊢ ∪x ∈ A B = ∪y ∈ A C
Theorem	cbviin 4005*	Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ ℲyB    &   ⊢ ℲxC    &   ⊢ (x = y → B = C)    ⇒   ⊢ ∩x ∈ A B = ∩y ∈ A C
Theorem	cbviunv 4006*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 15-Sep-2003.)
⊢ (x = y → B = C)    ⇒   ⊢ ∪x ∈ A B = ∪y ∈ A C
Theorem	cbviinv 4007*	Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.)
⊢ (x = y → B = C)    ⇒   ⊢ ∩x ∈ A B = ∩y ∈ A C
Theorem	iunss 4008*	Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∪x ∈ A B ⊆ C ↔ ∀x ∈ A B ⊆ C)
Theorem	ssiun 4009*	Subset implication for an indexed union. (Contributed by NM, 3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∃x ∈ A C ⊆ B → C ⊆ ∪x ∈ A B)
Theorem	ssiun2 4010	Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (x ∈ A → B ⊆ ∪x ∈ A B)
Theorem	ssiun2s 4011*	Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.)
⊢ (x = C → B = D)    ⇒   ⊢ (C ∈ A → D ⊆ ∪x ∈ A B)
Theorem	iunss2 4012*	A subclass condition on the members of two indexed classes C(x) and D(y) that implies a subclass relation on their indexed unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59. Compare uniss2 3923. (Contributed by NM, 9-Dec-2004.)
⊢ (∀x ∈ A ∃y ∈ B C ⊆ D → ∪x ∈ A C ⊆ ∪y ∈ B D)
Theorem	iunab 4013*	The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004.)
⊢ ∪x ∈ A {y ∣ φ} = {y ∣ ∃x ∈ A φ}
Theorem	iunrab 4014*	The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
⊢ ∪x ∈ A {y ∈ B ∣ φ} = {y ∈ B ∣ ∃x ∈ A φ}
Theorem	iunxdif2 4015*	Indexed union with a class difference as its index. (Contributed by NM, 10-Dec-2004.)
⊢ (x = y → C = D)    ⇒   ⊢ (∀x ∈ A ∃y ∈ (A ∖ B)C ⊆ D → ∪y ∈ (A ∖ B)D = ∪x ∈ A C)
Theorem	ssiinf 4016	Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.)
⊢ ℲxC    ⇒   ⊢ (C ⊆ ∩x ∈ A B ↔ ∀x ∈ A C ⊆ B)
Theorem	ssiin 4017*	Subset theorem for an indexed intersection. (Contributed by NM, 15-Oct-2003.)
⊢ (C ⊆ ∩x ∈ A B ↔ ∀x ∈ A C ⊆ B)
Theorem	iinss 4018*	Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∃x ∈ A B ⊆ C → ∩x ∈ A B ⊆ C)
Theorem	iinss2 4019	An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012.)
⊢ (x ∈ A → ∩x ∈ A B ⊆ B)
Theorem	uniiun 4020*	Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.)
⊢ ∪A = ∪x ∈ A x
Theorem	intiin 4021*	Class intersection in terms of indexed intersection. Definition in [Stoll] p. 44. (Contributed by NM, 28-Jun-1998.)
⊢ ∩A = ∩x ∈ A x
Theorem	iunid 4022*	An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.)
⊢ ∪x ∈ A {x} = A
Theorem	iun0 4023	An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ∪x ∈ A ∅ = ∅
Theorem	0iun 4024	An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ∪x ∈ ∅ A = ∅
Theorem	0iin 4025	An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005.)
⊢ ∩x ∈ ∅ A = V
Theorem	viin 4026*	Indexed intersection with a universal index class. When A doesn't depend on x, this evaluates to A by 19.3 1785 and abid2 2471. When A = x, this evaluates to ∅ by intiin 4021 and intv in set.mm. (Contributed by NM, 11-Sep-2008.)
⊢ ∩x ∈ V A = {y ∣ ∀x y ∈ A}
Theorem	iunn0 4027*	There is a nonempty class in an indexed collection B(x) iff the indexed union of them is nonempty. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∃x ∈ A B ≠ ∅ ↔ ∪x ∈ A B ≠ ∅)
Theorem	iinab 4028*	Indexed intersection of a class builder. (Contributed by NM, 6-Dec-2011.)
⊢ ∩x ∈ A {y ∣ φ} = {y ∣ ∀x ∈ A φ}
Theorem	iinrab 4029*	Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.)
⊢ (A ≠ ∅ → ∩x ∈ A {y ∈ B ∣ φ} = {y ∈ B ∣ ∀x ∈ A φ})
Theorem	iinrab2 4030*	Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.)
⊢ (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = {y ∈ B ∣ ∀x ∈ A φ}
Theorem	iunin2 4031*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4020 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
⊢ ∪x ∈ A (B ∩ C) = (B ∩ ∪x ∈ A C)
Theorem	iunin1 4032*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4020 to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ∪x ∈ A (C ∩ B) = (∪x ∈ A C ∩ B)
Theorem	iinun2 4033*	Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4021 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
⊢ ∩x ∈ A (B ∪ C) = (B ∪ ∩x ∈ A C)
Theorem	iundif2 4034*	Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 4021 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
⊢ ∪x ∈ A (B ∖ C) = (B ∖ ∩x ∈ A C)
Theorem	2iunin 4035*	Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008.)
⊢ ∪x ∈ A ∪y ∈ B (C ∩ D) = (∪x ∈ A C ∩ ∪y ∈ B D)
Theorem	iindif2 4036*	Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 4020 to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006.)
⊢ (A ≠ ∅ → ∩x ∈ A (B ∖ C) = (B ∖ ∪x ∈ A C))
Theorem	iinin2 4037*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4021 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (A ≠ ∅ → ∩x ∈ A (B ∩ C) = (B ∩ ∩x ∈ A C))
Theorem	iinin1 4038*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4021 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (A ≠ ∅ → ∩x ∈ A (C ∩ B) = (∩x ∈ A C ∩ B))
Theorem	elriin 4039*	Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (B ∈ (A ∩ ∩x ∈ X S) ↔ (B ∈ A ∧ ∀x ∈ X B ∈ S))
Theorem	riin0 4040*	Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (X = ∅ → (A ∩ ∩x ∈ X S) = A)
Theorem	riinn0 4041*	Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((∀x ∈ X S ⊆ A ∧ X ≠ ∅) → (A ∩ ∩x ∈ X S) = ∩x ∈ X S)
Theorem	riinrab 4042*	Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (A ∩ ∩x ∈ X {y ∈ A ∣ φ}) = {y ∈ A ∣ ∀x ∈ X φ}
Theorem	iinxsng 4043*	A singleton index picks out an instance of an indexed intersection's argument. (Contributed by NM, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ (x = A → B = C)    ⇒   ⊢ (A ∈ V → ∩x ∈ {A}B = C)
Theorem	iinxprg 4044*	Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.)
⊢ (x = A → C = D)    &   ⊢ (x = B → C = E)    ⇒   ⊢ ((A ∈ V ∧ B ∈ W) → ∩x ∈ {A, B}C = (D ∩ E))
Theorem	iunxsng 4045*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.)
⊢ (x = A → B = C)    ⇒   ⊢ (A ∈ V → ∪x ∈ {A}B = C)
Theorem	iunxsn 4046*	A singleton index picks out an instance of an indexed union's argument. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 25-Jun-2016.)
⊢ A ∈ V    &   ⊢ (x = A → B = C)    ⇒   ⊢ ∪x ∈ {A}B = C
Theorem	iunun 4047	Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ ∪x ∈ A (B ∪ C) = (∪x ∈ A B ∪ ∪x ∈ A C)
Theorem	iunxun 4048	Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ ∪x ∈ (A ∪ B)C = (∪x ∈ A C ∪ ∪x ∈ B C)
Theorem	iunxiun 4049*	Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.)
⊢ ∪x ∈ ∪ y ∈ A BC = ∪y ∈ A ∪x ∈ B C
Theorem	iinuni 4050*	A relationship involving union and indexed intersection. Exercise 23 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ (A ∪ ∩B) = ∩x ∈ B (A ∪ x)
Theorem	iununi 4051*	A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ ((B = ∅ → A = ∅) ↔ (A ∪ ∪B) = ∪x ∈ B (A ∪ x))
Theorem	sspwuni 4052	Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
⊢ (A ⊆ ℘B ↔ ∪A ⊆ B)
Theorem	pwssb 4053*	Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.)
⊢ (A ⊆ ℘B ↔ ∀x ∈ A x ⊆ B)
Theorem	elpwuni 4054	Relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
⊢ (B ∈ A → (A ⊆ ℘B ↔ ∪A = B))
Theorem	iinpw 4055*	The power class of an intersection in terms of indexed intersection. Exercise 24(a) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.)
⊢ ℘∩A = ∩x ∈ A ℘x
Theorem	iunpwss 4056*	Inclusion of an indexed union of a power class in the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.)
⊢ ∪x ∈ A ℘x ⊆ ℘∪A
Theorem	rintn0 4057	Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Revised by Mario Carneiro, 5-Jun-2015.)
⊢ ((X ⊆ ℘A ∧ X ≠ ∅) → (A ∩ ∩X) = ∩X)
2.1.20  The Kuratowski ordered pair
Syntax	copk 4058	Extend class notation to include Kuratowski ordered pair.
class ⟪A, B⟫
Definition	df-opk 4059	Define the Kuratowski ordered pair. This ordered pair definition is standard for ZFC set theory, but we do not use it beyond establishing df-op 4567, since it is not type-level. We state this definition since it is a simple definition that can be used by the set construction axioms that follow this section. (Contributed by SF, 12-Jan-2015.)
⊢ ⟪A, B⟫ = {{A}, {A, B}}
Theorem	opkeq1 4060	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.)
⊢ (A = B → ⟪A, C⟫ = ⟪B, C⟫)
Theorem	opkeq2 4061	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.)
⊢ (A = B → ⟪C, A⟫ = ⟪C, B⟫)
Theorem	opkeq12 4062	Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
⊢ ((A = C ∧ B = D) → ⟪A, B⟫ = ⟪C, D⟫)
Theorem	opkeq1i 4063	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ A = B    ⇒   ⊢ ⟪A, C⟫ = ⟪B, C⟫
Theorem	opkeq2i 4064	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ A = B    ⇒   ⊢ ⟪C, A⟫ = ⟪C, B⟫
Theorem	opkeq12i 4065	Equality inference for ordered pairs. (The proof was shortened by Eric Schmidt, 4-Apr-2007.) (Contributed by NM, 16-Dec-2006.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ ⟪A, C⟫ = ⟪B, D⟫
Theorem	opkeq1d 4066	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ⟪A, C⟫ = ⟪B, C⟫)
Theorem	opkeq2d 4067	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ⟪C, A⟫ = ⟪C, B⟫)
Theorem	opkeq12d 4068	Equality deduction for ordered pairs. (The proof was shortened by Andrew Salmon, 29-Jun-2011.) (Contributed by NM, 16-Dec-2006.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → ⟪A, C⟫ = ⟪B, D⟫)
Theorem	nfopk 4069	Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx⟪A, B⟫
2.1.21  More Boolean set operations
Theorem	compldif 4070	Complement in terms of difference. (Contributed by SF, 2-Jan-2018.)
⊢ ∼ A = (V ∖ A)
Theorem	complV 4071	The complement of the universe is the empty set. (Contributed by SF, 2-Jan-2018.)
⊢ ∼ V = ∅
Theorem	compl0 4072	The complement of the empty set is the universe. (Contributed by SF, 2-Jan-2018.)
⊢ ∼ ∅ = V
Theorem	nincompl 4073	Anti-intersection with complement. (Contributed by SF, 2-Jan-2018.)
⊢ (A ⩃ ∼ A) = V
Theorem	incompl 4074	Intersection with complement. (Contributed by SF, 2-Jan-2018.)
⊢ (A ∩ ∼ A) = ∅
Theorem	uncompl 4075	Union with complement. (Contributed by SF, 2-Jan-2018.)
⊢ (A ∪ ∼ A) = V
Theorem	inindif 4076	The intersection of an intersection and a difference is empty. (Contributed by set.mm contributors, 10-Mar-2015.)
⊢ ((A ∩ B) ∩ (A ∖ B)) = ∅
Theorem	ssofss 4077*	Condition for subset when A is already known to be a subset. (Contributed by SF, 13-Jan-2015.)
⊢ (A ⊆ C → (A ⊆ B ↔ ∀x ∈ C (x ∈ A → x ∈ B)))
Theorem	ssofeq 4078*	When A and B are subsets of C, equality depends only on the elements of C. (Contributed by SF, 13-Jan-2015.)
⊢ ((A ⊆ C ∧ B ⊆ C) → (A = B ↔ ∀x ∈ C (x ∈ A ↔ x ∈ B)))
2.2  NF Set Theory - add the Set Construction Axioms
2.2.1  Introduce the set construction axioms
Axiom	ax-nin 4079*	State the axiom of anti-intersection. Axiom P1 of [Hailperin] p. 6. This axiom sets up boolean operations on sets. Note on this and the following axioms: this axiom, ax-xp 4080, ax-cnv 4081, ax-1c 4082, ax-sset 4083, ax-si 4084, ax-ins2 4085, ax-ins3 4086, and ax-typlower 4087 are from Hailperin and are designed to implement the Stratification Axiom of Quine. A well-formed formula using only propositional symbols, predicate symbols, and ∈ is "stratified" iff you can make a (metalogical) mapping from the variables to the natural numbers such that any formulas of the form x = y have the same number, and any formulas of the form x ∈ y have x as one less than y. Quine's stratification axiom states that there is a set corresponding to any stratified formula. Since we cannot state stratification from within the logic, we use Hailperin's axioms and prove existence of stratified sets using Hailperin's algorithm. (Contributed by SF, 12-Jan-2015.)
⊢ ∃z∀w(w ∈ z ↔ (w ∈ x ⊼ w ∈ y))
Axiom	ax-xp 4080*	State the axiom of cross product. This axiom guarantees the existence of the (Kuratowski) cross product of V with x. Axiom P5 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
⊢ ∃y∀z(z ∈ y ↔ ∃w∃t(z = ⟪w, t⟫ ∧ t ∈ x))
Axiom	ax-cnv 4081*	State the axiom of converse. This axiom guarantees the existence of the Kuratowski converse of x. Axiom P7 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
⊢ ∃y∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x)
Axiom	ax-1c 4082*	State the axiom of cardinal one. This axiom guarantees the existence of the set of all singletons, which will become cardinal one later in our development. Axiom P8 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
⊢ ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z))
Axiom	ax-sset 4083*	State the axiom of the subset relationship. This axiom guarantees the existence of the Kuratowski relationship representing subset. Slight generalization of axiom P9 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
⊢ ∃x∀y∀z(⟪y, z⟫ ∈ x ↔ ∀w(w ∈ y → w ∈ z))
Axiom	ax-si 4084*	State the axiom of the singleton image. This axiom guarantees that guarantees the existence of a set that raises the "type" of another set when considered as a relationship. Axiom P2 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
⊢ ∃y∀z∀w(⟪{z}, {w}⟫ ∈ y ↔ ⟪z, w⟫ ∈ x)
Axiom	ax-ins2 4085*	State the insertion two axiom. This axiom sets up a set that inserts an extra variable at the second place of the relationship described by x. Axiom P3 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x)
Axiom	ax-ins3 4086*	State the insertion three axiom. This axiom sets up a set that inserts an extra variable at the third place of the relationship described by x. Axiom P4 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, w⟫ ∈ x)
Axiom	ax-typlower 4087*	The type lowering axiom. This axiom eventually sets up both the existence of the sum set and the existence of the range of a relationship. Axiom P6 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
⊢ ∃y∀z(z ∈ y ↔ ∀w⟪w, {z}⟫ ∈ x)
Axiom	ax-sn 4088*	The singleton axiom. This axiom sets up the existence of a singleton set. This appears to have been an oversight on Hailperin's part, as it is needed to prove the properties of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)
⊢ ∃y∀z(z ∈ y ↔ z = x)
2.2.2  Primitive forms for some axioms
Theorem	axprimlem1 4089*	Lemma for the primitive axioms. Primitive form of equality to a singleton. (Contributed by SF, 25-Mar-2015.)
⊢ (a = {B} ↔ ∀c(c ∈ a ↔ c = B))
Theorem	axprimlem2 4090*	Lemma for the primitive axioms. Primitive form of equality to a Kuratowski ordered pair. (Contributed by SF, 25-Mar-2015.)
⊢ (a = ⟪B, C⟫ ↔ ∀d(d ∈ a ↔ (∀e(e ∈ d ↔ e = B) ∨ ∀f(f ∈ d ↔ (f = B ∨ f = C)))))
Theorem	axxpprim 4091*	ax-xp 4080 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
⊢ ∃y∀z(z ∈ y ↔ ∃w∃t(∀a(a ∈ z ↔ (∀b(b ∈ a ↔ b = w) ∨ ∀c(c ∈ a ↔ (c = w ∨ c = t)))) ∧ t ∈ x))
Theorem	axcnvprim 4092*	ax-cnv 4081 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
⊢ ∃y∀z∀w(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ c = z) ∨ ∀d(d ∈ b ↔ (d = z ∨ d = w)))) ∧ a ∈ y) ↔ ∃e(∀f(f ∈ e ↔ (∀g(g ∈ f ↔ g = w) ∨ ∀h(h ∈ f ↔ (h = w ∨ h = z)))) ∧ e ∈ x))
Theorem	axssetprim 4093*	ax-sset 4083 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
⊢ ∃x∀y∀z(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ c = y) ∨ ∀d(d ∈ b ↔ (d = y ∨ d = z)))) ∧ a ∈ x) ↔ ∀e(e ∈ y → e ∈ z))
Theorem	axsiprim 4094*	ax-si 4084 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
⊢ ∃y∀z∀w(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ d = z)) ∨ ∀e(e ∈ b ↔ (∀f(f ∈ e ↔ f = z) ∨ ∀g(g ∈ e ↔ g = w))))) ∧ a ∈ y) ↔ ∃h(∀i(i ∈ h ↔ (∀j(j ∈ i ↔ j = z) ∨ ∀k(k ∈ i ↔ (k = z ∨ k = w)))) ∧ h ∈ x))
Theorem	axtyplowerprim 4095*	ax-typlower 4087 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
⊢ ∃y∀z(z ∈ y ↔ ∀w∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ c = w) ∨ ∀d(d ∈ b ↔ (d = w ∨ ∀e(e ∈ d ↔ e = z))))) ∧ a ∈ x))
Theorem	axins2prim 4096*	ax-ins2 4085 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
⊢ ∃y∀z∀w∀t(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y) ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = t)))) ∧ k ∈ x))
Theorem	axins3prim 4097*	ax-ins3 4086 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
⊢ ∃y∀z∀w∀t(∃a(∀b(b ∈ a ↔ (∀c(c ∈ b ↔ ∀d(d ∈ c ↔ ∀e(e ∈ d ↔ e = z))) ∨ ∀f(f ∈ b ↔ (∀g(g ∈ f ↔ ∀e(e ∈ g ↔ e = z)) ∨ ∀h(h ∈ f ↔ (∀i(i ∈ h ↔ i = w) ∨ ∀j(j ∈ h ↔ (j = w ∨ j = t)))))))) ∧ a ∈ y) ↔ ∃k(∀l(l ∈ k ↔ (∀m(m ∈ l ↔ m = z) ∨ ∀n(n ∈ l ↔ (n = z ∨ n = w)))) ∧ k ∈ x))
2.2.3  Initial existence theorems
Theorem	ninexg 4098	The anti-intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A ⩃ B) ∈ V)
Theorem	ninex 4099	The anti-intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ⩃ B) ∈ V
Theorem	complexg 4100	The complement of a set is a set. (Contributed by SF, 12-Jan-2015.)
⊢ (A ∈ V → ∼ A ∈ V)