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	dfiun2 4001*	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 4002*	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 4003*	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 4004*	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 4005*	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 4006*	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 4007*	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 4008*	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 4009	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 4010*	Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.)
⊢ (x = C → B = D)    ⇒   ⊢ (C ∈ A → D ⊆ ∪x ∈ A B)
Theorem	iunss2 4011*	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 3922. (Contributed by NM, 9-Dec-2004.)
⊢ (∀x ∈ A ∃y ∈ B C ⊆ D → ∪x ∈ A C ⊆ ∪y ∈ B D)
Theorem	iunab 4012*	The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004.)
⊢ ∪x ∈ A {y ∣ φ} = {y ∣ ∃x ∈ A φ}
Theorem	iunrab 4013*	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 4014*	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 4015	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 4016*	Subset theorem for an indexed intersection. (Contributed by NM, 15-Oct-2003.)
⊢ (C ⊆ ∩x ∈ A B ↔ ∀x ∈ A C ⊆ B)
Theorem	iinss 4017*	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 4018	An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012.)
⊢ (x ∈ A → ∩x ∈ A B ⊆ B)
Theorem	uniiun 4019*	Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.)
⊢ ∪A = ∪x ∈ A x
Theorem	intiin 4020*	Class intersection in terms of indexed intersection. Definition in [Stoll] p. 44. (Contributed by NM, 28-Jun-1998.)
⊢ ∩A = ∩x ∈ A x
Theorem	iunid 4021*	An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.)
⊢ ∪x ∈ A {x} = A
Theorem	iun0 4022	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 4023	An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ∪x ∈ ∅ A = ∅
Theorem	0iin 4024	An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005.)
⊢ ∩x ∈ ∅ A = V
Theorem	viin 4025*	Indexed intersection with a universal index class. When A doesn't depend on x, this evaluates to A by 19.3 1785 and abid2 2470. When A = x, this evaluates to ∅ by intiin 4020 and intv in set.mm. (Contributed by NM, 11-Sep-2008.)
⊢ ∩x ∈ V A = {y ∣ ∀x y ∈ A}
Theorem	iunn0 4026*	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 4027*	Indexed intersection of a class builder. (Contributed by NM, 6-Dec-2011.)
⊢ ∩x ∈ A {y ∣ φ} = {y ∣ ∀x ∈ A φ}
Theorem	iinrab 4028*	Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.)
⊢ (A ≠ ∅ → ∩x ∈ A {y ∈ B ∣ φ} = {y ∈ B ∣ ∀x ∈ A φ})
Theorem	iinrab2 4029*	Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.)
⊢ (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = {y ∈ B ∣ ∀x ∈ A φ}
Theorem	iunin2 4030*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4019 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
⊢ ∪x ∈ A (B ∩ C) = (B ∩ ∪x ∈ A C)
Theorem	iunin1 4031*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4019 to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ∪x ∈ A (C ∩ B) = (∪x ∈ A C ∩ B)
Theorem	iinun2 4032*	Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4020 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
⊢ ∩x ∈ A (B ∪ C) = (B ∪ ∩x ∈ A C)
Theorem	iundif2 4033*	Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 4020 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
⊢ ∪x ∈ A (B ∖ C) = (B ∖ ∩x ∈ A C)
Theorem	2iunin 4034*	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 4035*	Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 4019 to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006.)
⊢ (A ≠ ∅ → ∩x ∈ A (B ∖ C) = (B ∖ ∪x ∈ A C))
Theorem	iinin2 4036*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4020 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (A ≠ ∅ → ∩x ∈ A (B ∩ C) = (B ∩ ∩x ∈ A C))
Theorem	iinin1 4037*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4020 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (A ≠ ∅ → ∩x ∈ A (C ∩ B) = (∩x ∈ A C ∩ B))
Theorem	elriin 4038*	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 4039*	Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (X = ∅ → (A ∩ ∩x ∈ X S) = A)
Theorem	riinn0 4040*	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 4041*	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 4042*	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 4043*	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 4044*	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 4045*	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 4046	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 4047	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 4048*	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 4049*	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 4050*	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 4051	Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
⊢ (A ⊆ ℘B ↔ ∪A ⊆ B)
Theorem	pwssb 4052*	Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.)
⊢ (A ⊆ ℘B ↔ ∀x ∈ A x ⊆ B)
Theorem	elpwuni 4053	Relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
⊢ (B ∈ A → (A ⊆ ℘B ↔ ∪A = B))
Theorem	iinpw 4054*	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 4055*	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 4056	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 4057	Extend class notation to include Kuratowski ordered pair.
class ⟪A, B⟫
Definition	df-opk 4058	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 4566, 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 4059	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.)
⊢ (A = B → ⟪A, C⟫ = ⟪B, C⟫)
Theorem	opkeq2 4060	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.)
⊢ (A = B → ⟪C, A⟫ = ⟪C, B⟫)
Theorem	opkeq12 4061	Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
⊢ ((A = C ∧ B = D) → ⟪A, B⟫ = ⟪C, D⟫)
Theorem	opkeq1i 4062	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ A = B    ⇒   ⊢ ⟪A, C⟫ = ⟪B, C⟫
Theorem	opkeq2i 4063	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ A = B    ⇒   ⊢ ⟪C, A⟫ = ⟪C, B⟫
Theorem	opkeq12i 4064	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 4065	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ⟪A, C⟫ = ⟪B, C⟫)
Theorem	opkeq2d 4066	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ⟪C, A⟫ = ⟪C, B⟫)
Theorem	opkeq12d 4067	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 4068	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 4069	Complement in terms of difference. (Contributed by SF, 2-Jan-2018.)
⊢ ∼ A = (V ∖ A)
Theorem	complV 4070	The complement of the universe is the empty set. (Contributed by SF, 2-Jan-2018.)
⊢ ∼ V = ∅
Theorem	compl0 4071	The complement of the empty set is the universe. (Contributed by SF, 2-Jan-2018.)
⊢ ∼ ∅ = V
Theorem	nincompl 4072	Anti-intersection with complement. (Contributed by SF, 2-Jan-2018.)
⊢ (A ⩃ ∼ A) = V
Theorem	incompl 4073	Intersection with complement. (Contributed by SF, 2-Jan-2018.)
⊢ (A ∩ ∼ A) = ∅
Theorem	uncompl 4074	Union with complement. (Contributed by SF, 2-Jan-2018.)
⊢ (A ∪ ∼ A) = V
Theorem	inindif 4075	The intersection of an intersection and a difference is empty. (Contributed by set.mm contributors, 10-Mar-2015.)
⊢ ((A ∩ B) ∩ (A ∖ B)) = ∅
Theorem	ssofss 4076*	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 4077*	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 4078*	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 4079, ax-cnv 4080, ax-1c 4081, ax-sset 4082, ax-si 4083, ax-ins2 4084, ax-ins3 4085, and ax-typlower 4086 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 4079*	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 4080*	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 4081*	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 4082*	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 4083*	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 4084*	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 4085*	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 4086*	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 4087*	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 4088*	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 4089*	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 4090*	ax-xp 4079 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 4091*	ax-cnv 4080 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 4092*	ax-sset 4082 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 4093*	ax-si 4083 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 4094*	ax-typlower 4086 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 4095*	ax-ins2 4084 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 4096*	ax-ins3 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 = w)))) ∧ k ∈ x))
2.2.3  Initial existence theorems
Theorem	ninexg 4097	The anti-intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A ⩃ B) ∈ V)
Theorem	ninex 4098	The anti-intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ⩃ B) ∈ V
Theorem	complexg 4099	The complement of a set is a set. (Contributed by SF, 12-Jan-2015.)
⊢ (A ∈ V → ∼ A ∈ V)
Theorem	inexg 4100	The intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A ∩ B) ∈ V)