Type  Label  Description 
Statement 

Theorem  unexg 4101 
The union of two sets is a set. (Contributed by SF, 12Jan2015.)

⊢ ((A ∈ V ∧ B ∈ W) →
(A ∪ B) ∈
V) 

Theorem  difexg 4102 
The difference of two sets is a set. (Contributed by SF, 12Jan2015.)

⊢ ((A ∈ V ∧ B ∈ W) →
(A ∖
B) ∈
V) 

Theorem  symdifexg 4103 
The symmetric difference of two sets is a set. (Contributed by SF,
12Jan2015.)

⊢ ((A ∈ V ∧ B ∈ W) →
(A ⊕ B) ∈
V) 

Theorem  complex 4104 
The complement of a set is a set. (Contributed by SF, 12Jan2015.)

⊢ A ∈ V ⇒ ⊢ ∼ A
∈ V 

Theorem  inex 4105 
The intersection of two sets is a set. (Contributed by SF,
12Jan2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A ∩
B) ∈
V 

Theorem  unex 4106 
The union of two sets is a set. (Contributed by SF, 12Jan2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A ∪
B) ∈
V 

Theorem  difex 4107 
The difference of two sets is a set. (Contributed by SF,
12Jan2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A ∖ B) ∈ V 

Theorem  symdifex 4108 
The symmetric difference of two sets is a set. (Contributed by SF,
12Jan2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A ⊕
B) ∈
V 

Theorem  vvex 4109 
The universal class exists. This marks a major departure from ZFC set
theory, where V is a proper class. (Contributed by SF,
12Jan2015.)

⊢ V ∈
V 

Theorem  0ex 4110 
The empty class exists. (Contributed by SF, 12Jan2015.)

⊢ ∅ ∈ V 

Theorem  snex 4111 
A singleton always exists. (Contributed by SF, 12Jan2015.)

⊢ {A} ∈ V 

Theorem  prex 4112 
An unordered pair exists. (Contributed by SF, 12Jan2015.)

⊢ {A,
B} ∈
V 

Theorem  opkex 4113 
A Kuratowski ordered pair exists. (Contributed by SF, 12Jan2015.)

⊢ ⟪A,
B⟫ ∈ V 

Theorem  snelpwg 4114 
A singleton of a set belongs to a power class of a set containing it.
(Contributed by SF, 1Feb2015.)

⊢ (A ∈ V →
({A} ∈
℘B
↔ A ∈ B)) 

Theorem  snelpw 4115 
A singleton of a set belongs to a power class of a set containing it.
(Contributed by SF, 1Feb2015.)

⊢ A ∈ V ⇒ ⊢ ({A} ∈ ℘B ↔ A
∈ B) 

Theorem  snelpwi 4116 
A singleton of a set belongs to the power class of a class containing the
set. (Contributed by Alan Sare, 25Aug2011.)

⊢ (A ∈ B →
{A} ∈
℘B) 

Theorem  unipw 4117 
A class equals the union of its power class. Exercise 6(a) of
[Enderton] p. 38. (The proof was
shortened by Alan Sare, 28Dec2008.)
(Contributed by SF, 14Oct1996.) (Revised by SF, 29Dec2008.)

⊢ ∪℘A =
A 

Theorem  sspwb 4118 
Classes are subclasses if and only if their power classes are
subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by SF,
13Oct1996.)

⊢ (A ⊆ B ↔
℘A
⊆ ℘B) 

Theorem  pwadjoin 4119* 
Compute the power class of an adjoinment. (Contributed by SF,
30Jan2015.)

⊢ ℘(A ∪ {X}) =
(℘A
∪ {a ∣ ∃b ∈ ℘ Aa = (b ∪
{X})}) 

2.2.4 Singletons and pairs
(continued)


Theorem  snprss1 4120 
A singleton is a subset of an unordered pair. (Contributed by SF,
12Jan2015.)

⊢ {A} ⊆ {A,
B} 

Theorem  snprss2 4121 
A singleton is a subset of an unordered pair. (Contributed by SF,
12Jan2015.)

⊢ {A} ⊆ {B,
A} 

Theorem  prprc2 4122 
An unordered pair of a proper class. (Contributed by SF, 12Jan2015.)

⊢ (¬ A
∈ V → {B, A} =
{B}) 

Theorem  prprc1 4123 
An unordered pair of a proper class. (Contributed by SF, 12Jan2015.)

⊢ (¬ A
∈ V → {A, B} =
{B}) 

Theorem  preqr1 4124 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the first elements are equal. (Contributed by
NM, 18Oct1995.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ({A,
C} = {B, C} →
A = B) 

Theorem  preqr2 4125 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same first element, the second elements are equal. (Contributed by
NM, 5Aug1993.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ({C,
A} = {C, B} →
A = B) 

Theorem  preqr2g 4126 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same first element, the second elements are equal. (Contributed by
SF, 12Jan2015.)

⊢ ((A ∈ V ∧ B ∈ W) →
({C, A} = {C,
B} → A = B)) 

Theorem  preq12b 4127 
Equality relationship for two unordered pairs. (Contributed by NM,
17Oct1996.)

⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V ⇒ ⊢ ({A,
B} = {C, D} ↔
((A = C ∧ B = D) ∨ (A = D ∧ B = C))) 

Theorem  preq12bg 4128 
Closed form of preq12b 4127. (Contributed by Scott Fenton,
28Mar2014.)

⊢ (((A ∈ V ∧ B ∈ W) ∧ (C ∈ X ∧ D ∈ Y)) →
({A, B} = {C,
D} ↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C)))) 

2.2.5 Kuratowski ordered pairs
(continued)


Theorem  elopk 4129 
Membership in a Kuratowski ordered pair. (Contributed by SF,
12Jan2015.)

⊢ (A ∈ ⟪B,
C⟫ ↔ (A = {B} ∨ A = {B, C})) 

Theorem  opkth1g 4130 
Equality of the first member of a Kuratowski ordered pair, which holds
regardless of the sethood of the second members. (Contributed by SF,
12Jan2015.)

⊢ ((A ∈ V ∧ ⟪A,
B⟫ = ⟪C, D⟫)
→ A = C) 

Theorem  opkthg 4131 
Two Kuratowski ordered pairs are equal iff their components are equal.
(Contributed by SF, 12Jan2015.)

⊢ ((A ∈ V ∧ B ∈ W ∧ D ∈ T) →
(⟪A, B⟫ = ⟪C, D⟫
↔ (A = C ∧ B = D))) 

Theorem  opkth 4132 
Two Kuratowski ordered pairs are equal iff their components are equal.
(Contributed by SF, 12Jan2015.)

⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ D ∈ V ⇒ ⊢ (⟪A,
B⟫ = ⟪C, D⟫
↔ (A = C ∧ B = D)) 

2.2.6 Cardinal one, unit unions, and unit power
classes


Syntax  cuni1 4133 
Extend class notation to include the unit union of a class (read: 'unit
union A')

class
⋃_{1}A 

Syntax  c1c 4134 
Extend the definition of a class to include cardinal one.

class
1_{c} 

Syntax  cpw1 4135 
Extend class notation to include unit power class.

class
℘_{1}A 

Definition  df1c 4136* 
Define cardinal one. This is the set of all singletons, or the set of
all sets of size one. (Contributed by SF, 12Jan2015.)

⊢ 1_{c} = {x ∣ ∃y x = {y}} 

Definition  dfpw1 4137 
Define unit power class. Definition from [Rosser] p. 252. (Contributed
by SF, 12Jan2015.)

⊢ ℘_{1}A = (℘A ∩ 1_{c}) 

Definition  dfuni1 4138 
Define the unit union of a class. This operation is used implicitly in
both Holmes and Hailperin to complete their stratification algorithms,
although neither provide explicit notation for it. See eluni1 4173 for
membership condition. (Contributed by SF, 12Jan2015.)

⊢ ⋃_{1}A = ∪(A ∩ 1_{c}) 

Theorem  el1c 4139* 
Membership in cardinal one. (Contributed by SF, 12Jan2015.)

⊢ (A ∈ 1_{c} ↔ ∃x A = {x}) 

Theorem  snel1c 4140 
A singleton is an element of cardinal one. (Contributed by SF,
13Jan2015.)

⊢ A ∈ V ⇒ ⊢ {A} ∈ 1_{c} 

Theorem  snel1cg 4141 
A singleton is an element of cardinal one. (Contributed by SF,
30Jan2015.)

⊢ (A ∈ V →
{A} ∈
1_{c}) 

Theorem  1cex 4142 
Cardinal one is a set. (Contributed by SF, 12Jan2015.)

⊢ 1_{c} ∈ V 

Theorem  pw1eq 4143 
Equality theorem for unit power class. (Contributed by SF,
12Jan2015.)

⊢ (A =
B → ℘_{1}A = ℘_{1}B) 

Theorem  elpw1 4144* 
Membership in a unit power class. (Contributed by SF, 13Jan2015.)

⊢ (A ∈ ℘_{1}B ↔ ∃x ∈ B A = {x}) 

Theorem  elpw12 4145* 
Membership in a unit power class applied twice. (Contributed by SF,
15Jan2015.)

⊢ (A ∈ ℘_{1}℘_{1}B ↔ ∃x ∈ B A = {{x}}) 

Theorem  snelpw1 4146 
Membership of a singleton in a unit power class. (Contributed by SF,
13Jan2015.)

⊢ ({A} ∈ ℘_{1}B ↔ A
∈ B) 

Theorem  elpw11c 4147* 
Membership in ℘_{1}1_{c}.
(Contributed by SF, 13Jan2015.)

⊢ (A ∈ ℘_{1}1_{c} ↔ ∃x A = {{x}}) 

Theorem  elpw121c 4148* 
Membership in ℘_{1}℘_{1}1_{c}.
(Contributed by SF, 13Jan2015.)

⊢ (A ∈ ℘_{1}℘_{1}1_{c} ↔ ∃x A = {{{x}}}) 

Theorem  elpw131c 4149* 
Membership in ℘_{1}℘_{1}℘_{1}1_{c}.
(Contributed by SF, 14Jan2015.)

⊢ (A ∈ ℘_{1}℘_{1}℘_{1}1_{c} ↔ ∃x A = {{{{x}}}}) 

Theorem  elpw141c 4150* 
Membership in ℘_{1}℘_{1}℘_{1}℘_{1}1_{c}.
(Contributed by SF,
14Jan2015.)

⊢ (A ∈ ℘_{1}℘_{1}℘_{1}℘_{1}1_{c} ↔ ∃x A = {{{{{x}}}}}) 

Theorem  elpw151c 4151* 
Membership in ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c}.
(Contributed by SF,
14Jan2015.)

⊢ (A ∈ ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c} ↔ ∃x A = {{{{{{x}}}}}}) 

Theorem  elpw161c 4152* 
Membership in ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c}.
(Contributed by SF,
14Jan2015.)

⊢ (A ∈ ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c} ↔ ∃x A = {{{{{{{x}}}}}}}) 

Theorem  elpw171c 4153* 
Membership in ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c}.
(Contributed by SF,
15Jan2015.)

⊢ (A ∈ ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c} ↔ ∃x A = {{{{{{{{x}}}}}}}}) 

Theorem  elpw181c 4154* 
Membership in ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c}.
(Contributed by
SF, 15Jan2015.)

⊢ (A ∈ ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c} ↔ ∃x A = {{{{{{{{{x}}}}}}}}}) 

Theorem  elpw191c 4155* 
Membership in ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c}.
(Contributed
by SF, 24Jan2015.)

⊢ (A ∈ ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c} ↔ ∃x A = {{{{{{{{{{x}}}}}}}}}}) 

Theorem  elpw1101c 4156* 
Membership in ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c}.
(Contributed by SF, 24Jan2015.)

⊢ (A ∈ ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c} ↔ ∃x A = {{{{{{{{{{{x}}}}}}}}}}}) 

Theorem  elpw1111c 4157* 
Membership in ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c}.
(Contributed by SF, 24Jan2015.)

⊢ (A ∈ ℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}℘_{1}1_{c} ↔ ∃x A = {{{{{{{{{{{{x}}}}}}}}}}}}) 

Theorem  pw1ss1c 4158 
A unit power class is a subset of 1_{c}.
(Contributed by SF,
22Jan2015.)

⊢ ℘_{1}A ⊆
1_{c} 

Theorem  0nel1c 4159 
The empty class is not a singleton. (Contributed by SF, 22Jan2015.)

⊢ ¬ ∅
∈ 1_{c} 

Theorem  pw0 4160 
Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47.
(The proof was shortened by Andrew Salmon, 29Jun2011.) (Contributed by
SF, 5Aug1993.) (Revised by SF, 29Jun2011.)

⊢ ℘∅ = {∅} 

Theorem  pw10 4161 
Compute the unit power class of ∅. (Contributed by SF,
22Jan2015.)

⊢ ℘_{1}∅ = ∅ 

Theorem  eqpw1 4162* 
A condition for equality to unit power class. (Contributed by SF,
21Jan2015.)

⊢ (A = ℘_{1}B ↔ (A
⊆ 1_{c} ∧ ∀x({x} ∈ A ↔
x ∈
B))) 

Theorem  pw1un 4163 
Unit power class distributes over union. (Contributed by SF,
22Jan2015.)

⊢ ℘_{1}(A ∪ B) =
(℘_{1}A ∪ ℘_{1}B) 

Theorem  pw1in 4164 
Unit power class distributes over intersection. (Contributed by SF,
13Feb2015.)

⊢ ℘_{1}(A ∩ B) =
(℘_{1}A ∩ ℘_{1}B) 

Theorem  pw1sn 4165 
Compute the unit power class of a singleton. (Contributed by SF,
22Jan2015.)

⊢ A ∈ V ⇒ ⊢ ℘_{1}{A} = {{A}} 

Theorem  pw10b 4166 
The unit power class of a class is empty iff the class itself is empty.
(Contributed by SF, 22Jan2015.)

⊢ (℘_{1}A = ∅ ↔
A = ∅) 

Theorem  pw1disj 4167 
Two unit power classes are disjoint iff the classes themselves are
disjoint. (Contributed by SF, 26Jan2015.)

⊢ ((℘_{1}A ∩ ℘_{1}B) = ∅ ↔
(A ∩ B) = ∅) 

Theorem  df1c2 4168 
Cardinal one is the unit power class of the universe. (Contributed by
SF, 29Jan2015.)

⊢ 1_{c} = ℘_{1}V 

Theorem  pw1ss 4169 
Unit power set preserves subset. (Contributed by SF, 3Feb2015.)

⊢ (A ⊆ B →
℘_{1}A ⊆ ℘_{1}B) 

Theorem  pw111 4170 
The unit power class operation is onetoone. (Contributed by SF,
26Feb2015.)

⊢ (℘_{1}A = ℘_{1}B ↔ A =
B) 

Theorem  pw1sspw 4171 
A unit power class is a subset of a power class. (Contributed by SF,
10Mar2015.)

⊢ ℘_{1}A ⊆ ℘A 

Theorem  eluni1g 4172 
Membership in a unit union. (Contributed by SF, 15Mar2015.)

⊢ (A ∈ V →
(A ∈
⋃_{1}B ↔ {A} ∈ B)) 

Theorem  eluni1 4173 
Membership in a unit union. (Contributed by SF, 15Mar2015.)

⊢ A ∈ V ⇒ ⊢ (A ∈ ⋃_{1}B ↔ {A}
∈ B) 

2.2.7 Kuratowski relationships


Syntax  cxpk 4174 
Extend the definition of a class to include the Kuratowski cross
product.

class
(A ×_{k}
B) 

Syntax  ccnvk 4175 
Extend the definition of a class to include the Kuratowski converse of a
class.

class
^{◡}_{k}A 

Syntax  cins2k 4176 
Extend the definition of a class to include the Kuratowski second
insertion operator.

class
Ins2_{k} A 

Syntax  cins3k 4177 
Extend the definition of a class to include the Kuratowski third insertion
operator.

class
Ins3_{k} A 

Syntax  cp6 4178 
Extend the definition of a class to include the P6 operator (the set
guaranteed by axtyplower 4086).

class
P6 A 

Syntax  cimak 4179 
Extend the definition of a class to include the Kuratowski image of a
class. (Read: The image of B under A.)

class
(A “_{k}
B) 

Syntax  ccomk 4180 
Extend the definition of a class to include the Kuratowski composition of
two classes. (Read: The composition of A and B.)

class
(A ∘_{k} B) 

Syntax  csik 4181 
Extend the definition of a class to include the Kuratowski singleton
image.

class
SI_{k} A 

Syntax  cimagek 4182 
Extend the definition of a class to include the Kuratowski image
functor.

class
Image_{k}A 

Syntax  cssetk 4183 
Extend the definition of a class to include the Kuratowski subset
relationship.

class
S_{k} 

Syntax  cidk 4184 
Extend the definition of a class to include the Kuratowski identity
relationship.

class
I_{k} 

Definition  dfxpk 4185* 
Define the Kuratowski cross product. This definition through dfidk 4195
set up the Kuratowski relationships. These are used mainly to prove the
properties of dfop 4566, and are not used thereafter. (Contributed
by
SF, 12Jan2015.)

⊢ (A
×_{k} B) = {x ∣ ∃y∃z(x = ⟪y,
z⟫ ∧ (y ∈ A ∧ z ∈ B))} 

Definition  dfcnvk 4186* 
Define the Kuratowski converse. (Contributed by SF, 12Jan2015.)

⊢ ^{◡}_{k}A = {x ∣ ∃y∃z(x =
⟪y, z⟫ ∧
⟪z, y⟫ ∈
A)} 

Definition  dfins2k 4187* 
Define the Kuratowski second insertion operator. (Contributed by SF,
12Jan2015.)

⊢ Ins2_{k} A = {x ∣ ∃y∃z(x =
⟪y, z⟫ ∧ ∃t∃u∃v(y = {{t}} ∧ z =
⟪u, v⟫ ∧
⟪t, v⟫ ∈
A))} 

Definition  dfins3k 4188* 
Define the Kuratowski third insertion operator. (Contributed by SF,
12Jan2015.)

⊢ Ins3_{k} A = {x ∣ ∃y∃z(x =
⟪y, z⟫ ∧ ∃t∃u∃v(y = {{t}} ∧ z =
⟪u, v⟫ ∧
⟪t, u⟫ ∈
A))} 

Definition  dfimak 4189* 
Define the Kuratowski image operator. (Contributed by SF,
12Jan2015.)

⊢ (A
“_{k} B) = {x ∣ ∃y ∈ B
⟪y, x⟫ ∈
A} 

Definition  dfcok 4190 
Define the Kuratowski composition operator. (Contributed by SF,
12Jan2015.)

⊢ (A ∘_{k} B) = (( Ins2_{k} A ∩ Ins3_{k} ^{◡}_{k}B) “_{k} V) 

Definition  dfp6 4191* 
Define the P6 operator. This is the set guaranteed by axtyplower 4086.
(Contributed by SF, 12Jan2015.)

⊢ P6 A = {x ∣ (V ×_{k} {{x}}) ⊆ A} 

Definition  dfsik 4192* 
Define the Kuratowski singleton image operation. (Contributed by SF,
12Jan2015.)

⊢ SI_{k} A = {x ∣ ∃y∃z(x =
⟪y, z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧
⟪t, u⟫ ∈
A))} 

Definition  dfssetk 4193* 
Define the Kuratowski subset relationship. (Contributed by SF,
12Jan2015.)

⊢ S_{k} = {x ∣ ∃y∃z(x = ⟪y,
z⟫ ∧ y ⊆ z)} 

Definition  dfimagek 4194 
Define the Kuratowski image function. See opkelimagek 4272 for membership.
(Contributed by SF, 12Jan2015.)

⊢ Image_{k}A = ((V ×_{k} V) ∖ (( Ins2_{k} S_{k} ⊕ Ins3_{k} ( S_{k} ∘_{k} ^{◡}_{k} SI_{k} A)) “_{k} ℘_{1}℘_{1}1_{c})) 

Definition  dfidk 4195* 
Define the Kuratowski identity relationship. (Contributed by SF,
12Jan2015.)

⊢ I_{k} = {x ∣ ∃y∃z(x = ⟪y,
z⟫ ∧ y = z)} 

Theorem  elxpk 4196* 
Membership in a Kuratowski cross product. (Contributed by SF,
12Jan2015.)

⊢ (A ∈ (B
×_{k} C) ↔ ∃x∃y(A = ⟪x,
y⟫ ∧ (x ∈ B ∧ y ∈ C))) 

Theorem  elxpk2 4197* 
Membership in a cross product. (Contributed by SF, 12Jan2015.)

⊢ (A ∈ (B
×_{k} C) ↔ ∃x ∈ B ∃y ∈ C A = ⟪x,
y⟫) 

Theorem  xpkeq1 4198 
Equality theorem for Kuratowski cross product. (Contributed by SF,
12Jan2015.)

⊢ (A =
B → (A ×_{k} C) = (B
×_{k} C)) 

Theorem  xpkeq2 4199 
Equality theorem for Kuratowski cross product. (Contributed by SF,
12Jan2015.)

⊢ (A =
B → (C ×_{k} A) = (C
×_{k} B)) 

Theorem  xpkeq12 4200 
Equality theorem for Kuratowski cross product. (Contributed by SF,
12Jan2015.)

⊢ ((A =
B ∧
C = D)
→ (A ×_{k}
C) = (B ×_{k} D)) 