Type  Label  Description 
Statement 

Theorem  elin3 3101 
Membership in a class defined as a ternary intersection. (Contributed
by Stefan O'Rear, 29Mar2015.)

⊢ 𝑋 = ((B
∩ 𝐶) ∩ 𝐷)
⇒ ⊢ (A ∈ 𝑋 ↔ (A ∈ B ∧ A ∈ 𝐶 ∧ A ∈ 𝐷)) 

Theorem  incom 3102 
Commutative law for intersection of classes. Exercise 7 of
[TakeutiZaring] p. 17.
(Contributed by NM, 5Aug1993.)

⊢ (A ∩
B) = (B ∩ A) 

Theorem  ineqri 3103* 
Inference from membership to intersection. (Contributed by NM,
5Aug1993.)

⊢ ((x ∈ A ∧ x ∈ B) ↔
x ∈
𝐶) ⇒ ⊢ (A ∩ B) =
𝐶 

Theorem  ineq1 3104 
Equality theorem for intersection of two classes. (Contributed by NM,
14Dec1993.)

⊢ (A =
B → (A ∩ 𝐶) = (B
∩ 𝐶)) 

Theorem  ineq2 3105 
Equality theorem for intersection of two classes. (Contributed by NM,
26Dec1993.)

⊢ (A =
B → (𝐶 ∩ A) = (𝐶 ∩ B)) 

Theorem  ineq12 3106 
Equality theorem for intersection of two classes. (Contributed by NM,
8May1994.)

⊢ ((A =
B ∧ 𝐶 = 𝐷) → (A ∩ 𝐶) = (B
∩ 𝐷)) 

Theorem  ineq1i 3107 
Equality inference for intersection of two classes. (Contributed by NM,
26Dec1993.)

⊢ A =
B ⇒ ⊢ (A ∩ 𝐶) = (B
∩ 𝐶) 

Theorem  ineq2i 3108 
Equality inference for intersection of two classes. (Contributed by NM,
26Dec1993.)

⊢ A =
B ⇒ ⊢ (𝐶 ∩ A) = (𝐶 ∩ B) 

Theorem  ineq12i 3109 
Equality inference for intersection of two classes. (Contributed by
NM, 24Jun2004.) (Proof shortened by Eric Schmidt, 26Jan2007.)

⊢ A =
B & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (A ∩ 𝐶) = (B
∩ 𝐷) 

Theorem  ineq1d 3110 
Equality deduction for intersection of two classes. (Contributed by NM,
10Apr1994.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ → (A ∩ 𝐶) = (B
∩ 𝐶)) 

Theorem  ineq2d 3111 
Equality deduction for intersection of two classes. (Contributed by NM,
10Apr1994.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ → (𝐶 ∩ A) = (𝐶 ∩ B)) 

Theorem  ineq12d 3112 
Equality deduction for intersection of two classes. (Contributed by
NM, 24Jun2004.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ 𝐶 = 𝐷)
⇒ ⊢ (φ → (A ∩ 𝐶) = (B
∩ 𝐷)) 

Theorem  ineqan12d 3113 
Equality deduction for intersection of two classes. (Contributed by
NM, 7Feb2007.)

⊢ (φ
→ A = B)
& ⊢ (ψ
→ 𝐶 = 𝐷)
⇒ ⊢ ((φ ∧ ψ) → (A ∩ 𝐶) = (B
∩ 𝐷)) 

Theorem  dfss1 3114 
A frequentlyused variant of subclass definition dfss 2904. (Contributed
by NM, 10Jan2015.)

⊢ (A ⊆
B ↔ (B ∩ A) =
A) 

Theorem  dfss5 3115 
Another definition of subclasshood. Similar to dfss 2904, dfss 2905, and
dfss1 3114. (Contributed by David Moews, 1May2017.)

⊢ (A ⊆
B ↔ A = (B ∩
A)) 

Theorem  nfin 3116 
Boundvariable hypothesis builder for the intersection of classes.
(Contributed by NM, 15Sep2003.) (Revised by Mario Carneiro,
14Oct2016.)

⊢ ℲxA & ⊢
ℲxB ⇒ ⊢ Ⅎx(A ∩
B) 

Theorem  csbing 3117 
Distribute proper substitution through an intersection relation.
(Contributed by Alan Sare, 22Jul2012.)

⊢ (A ∈ B →
⦋A / x⦌(𝐶 ∩ 𝐷) = (⦋A / x⦌𝐶 ∩ ⦋A / x⦌𝐷)) 

Theorem  rabbi2dva 3118* 
Deduction from a wff to a restricted class abstraction. (Contributed by
NM, 14Jan2014.)

⊢ ((φ
∧ x ∈ A) →
(x ∈
B ↔ ψ)) ⇒ ⊢ (φ → (A ∩ B) =
{x ∈
A ∣ ψ}) 

Theorem  inidm 3119 
Idempotent law for intersection of classes. Theorem 15 of [Suppes]
p. 26. (Contributed by NM, 5Aug1993.)

⊢ (A ∩
A) = A 

Theorem  inass 3120 
Associative law for intersection of classes. Exercise 9 of
[TakeutiZaring] p. 17.
(Contributed by NM, 3May1994.)

⊢ ((A ∩
B) ∩ 𝐶) = (A
∩ (B ∩ 𝐶)) 

Theorem  in12 3121 
A rearrangement of intersection. (Contributed by NM, 21Apr2001.)

⊢ (A ∩
(B ∩ 𝐶)) = (B
∩ (A ∩ 𝐶)) 

Theorem  in32 3122 
A rearrangement of intersection. (Contributed by NM, 21Apr2001.)
(Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ((A ∩
B) ∩ 𝐶) = ((A
∩ 𝐶) ∩ B) 

Theorem  in13 3123 
A rearrangement of intersection. (Contributed by NM, 27Aug2012.)

⊢ (A ∩
(B ∩ 𝐶)) = (𝐶 ∩ (B ∩ A)) 

Theorem  in31 3124 
A rearrangement of intersection. (Contributed by NM, 27Aug2012.)

⊢ ((A ∩
B) ∩ 𝐶) = ((𝐶 ∩ B) ∩ A) 

Theorem  inrot 3125 
Rotate the intersection of 3 classes. (Contributed by NM,
27Aug2012.)

⊢ ((A ∩
B) ∩ 𝐶) = ((𝐶 ∩ A) ∩ B) 

Theorem  in4 3126 
Rearrangement of intersection of 4 classes. (Contributed by NM,
21Apr2001.)

⊢ ((A ∩
B) ∩ (𝐶 ∩ 𝐷)) = ((A ∩ 𝐶) ∩ (B ∩ 𝐷)) 

Theorem  inindi 3127 
Intersection distributes over itself. (Contributed by NM, 6May1994.)

⊢ (A ∩
(B ∩ 𝐶)) = ((A ∩ B)
∩ (A ∩ 𝐶)) 

Theorem  inindir 3128 
Intersection distributes over itself. (Contributed by NM,
17Aug2004.)

⊢ ((A ∩
B) ∩ 𝐶) = ((A
∩ 𝐶) ∩ (B ∩ 𝐶)) 

Theorem  sseqin2 3129 
A relationship between subclass and intersection. Similar to Exercise 9
of [TakeutiZaring] p. 18.
(Contributed by NM, 17May1994.)

⊢ (A ⊆
B ↔ (B ∩ A) =
A) 

Theorem  inss1 3130 
The intersection of two classes is a subset of one of them. Part of
Exercise 12 of [TakeutiZaring] p.
18. (Contributed by NM,
27Apr1994.)

⊢ (A ∩
B) ⊆ A 

Theorem  inss2 3131 
The intersection of two classes is a subset of one of them. Part of
Exercise 12 of [TakeutiZaring] p.
18. (Contributed by NM,
27Apr1994.)

⊢ (A ∩
B) ⊆ B 

Theorem  ssin 3132 
Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26.
(Contributed by NM, 15Jun2004.) (Proof shortened by Andrew Salmon,
26Jun2011.)

⊢ ((A ⊆
B ∧
A ⊆ 𝐶) ↔ A ⊆ (B
∩ 𝐶)) 

Theorem  ssini 3133 
An inference showing that a subclass of two classes is a subclass of
their intersection. (Contributed by NM, 24Nov2003.)

⊢ A ⊆
B & ⊢ A ⊆ 𝐶 ⇒ ⊢ A ⊆ (B
∩ 𝐶) 

Theorem  ssind 3134 
A deduction showing that a subclass of two classes is a subclass of
their intersection. (Contributed by Jonathan BenNaim, 3Jun2011.)

⊢ (φ
→ A ⊆ B)
& ⊢ (φ
→ A ⊆ 𝐶) ⇒ ⊢ (φ → A ⊆ (B
∩ 𝐶)) 

Theorem  ssrin 3135 
Add right intersection to subclass relation. (Contributed by NM,
16Aug1994.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (A ⊆
B → (A ∩ 𝐶) ⊆ (B ∩ 𝐶)) 

Theorem  sslin 3136 
Add left intersection to subclass relation. (Contributed by NM,
19Oct1999.)

⊢ (A ⊆
B → (𝐶 ∩ A) ⊆ (𝐶 ∩ B)) 

Theorem  ss2in 3137 
Intersection of subclasses. (Contributed by NM, 5May2000.)

⊢ ((A ⊆
B ∧ 𝐶 ⊆ 𝐷) → (A ∩ 𝐶) ⊆ (B ∩ 𝐷)) 

Theorem  ssinss1 3138 
Intersection preserves subclass relationship. (Contributed by NM,
14Sep1999.)

⊢ (A ⊆
𝐶 → (A ∩ B)
⊆ 𝐶) 

Theorem  inss 3139 
Inclusion of an intersection of two classes. (Contributed by NM,
30Oct2014.)

⊢ ((A ⊆
𝐶
∨ B ⊆ 𝐶) → (A ∩ B)
⊆ 𝐶) 

2.1.13.4 Combinations of difference, union, and
intersection of two classes


Theorem  unabs 3140 
Absorption law for union. (Contributed by NM, 16Apr2006.)

⊢ (A ∪
(A ∩ B)) = A 

Theorem  inabs 3141 
Absorption law for intersection. (Contributed by NM, 16Apr2006.)

⊢ (A ∩
(A ∪ B)) = A 

Theorem  nssinpss 3142 
Negation of subclass expressed in terms of intersection and proper
subclass. (Contributed by NM, 30Jun2004.) (Proof shortened by Andrew
Salmon, 26Jun2011.)

⊢ (¬ A
⊆ B ↔ (A ∩ B)
⊊ A) 

Theorem  nsspssun 3143 
Negation of subclass expressed in terms of proper subclass and union.
(Contributed by NM, 15Sep2004.)

⊢ (¬ A
⊆ B ↔ B ⊊ (A
∪ B)) 

Theorem  ssddif 3144 
Double complement and subset. Similar to ddifss 3148 but inside a class
B instead of
the universal class V. In classical logic the
subset operation on the right hand side could be an equality (that is,
A ⊆ B ↔ (B
∖ (B ∖ A)) = A).
(Contributed by Jim Kingdon,
24Jul2018.)

⊢ (A ⊆
B ↔ A ⊆ (B
∖ (B ∖ A))) 

Theorem  unssdif 3145 
Union of two classes and class difference. In classical logic this
would be an equality. (Contributed by Jim Kingdon, 24Jul2018.)

⊢ (A ∪
B) ⊆ (V ∖ ((V ∖ A) ∖ B)) 

Theorem  inssdif 3146 
Intersection of two classes and class difference. In classical logic
this would be an equality. (Contributed by Jim Kingdon,
24Jul2018.)

⊢ (A ∩
B) ⊆ (A ∖ (V ∖ B)) 

Theorem  difin 3147 
Difference with intersection. Theorem 33 of [Suppes] p. 29.
(Contributed by NM, 31Mar1998.) (Proof shortened by Andrew Salmon,
26Jun2011.)

⊢ (A ∖
(A ∩ B)) = (A
∖ B) 

Theorem  ddifss 3148 
Double complement under universal class. In classical logic (or given an
additional hypothesis, as in ddifnel 3048), this is equality rather than
subset. (Contributed by Jim Kingdon, 24Jul2018.)

⊢ A ⊆
(V ∖ (V ∖ A)) 

Theorem  unssin 3149 
Union as a subset of class complement and intersection (De Morgan's
law). One direction of the definition of union in [Mendelson] p. 231.
This would be an equality, rather than subset, in classical logic.
(Contributed by Jim Kingdon, 25Jul2018.)

⊢ (A ∪
B) ⊆ (V ∖ ((V ∖ A) ∩ (V ∖ B))) 

Theorem  inssun 3150 
Intersection in terms of class difference and union (De Morgan's law).
Similar to Exercise 4.10(n) of [Mendelson] p. 231. This would be an
equality, rather than subset, in classical logic. (Contributed by Jim
Kingdon, 25Jul2018.)

⊢ (A ∩
B) ⊆ (V ∖ ((V ∖ A) ∪ (V ∖ B))) 

Theorem  inssddif 3151 
Intersection of two classes and class difference. In classical logic,
such as Exercise 4.10(q) of [Mendelson]
p. 231, this is an equality rather
than subset. (Contributed by Jim Kingdon, 26Jul2018.)

⊢ (A ∩
B) ⊆ (A ∖ (A
∖ B)) 

Theorem  invdif 3152 
Intersection with universal complement. Remark in [Stoll] p. 20.
(Contributed by NM, 17Aug2004.)

⊢ (A ∩ (V
∖ B)) = (A ∖ B) 

Theorem  indif 3153 
Intersection with class difference. Theorem 34 of [Suppes] p. 29.
(Contributed by NM, 17Aug2004.)

⊢ (A ∩
(A ∖ B)) = (A
∖ B) 

Theorem  indif2 3154 
Bring an intersection in and out of a class difference. (Contributed by
Jeff Hankins, 15Jul2009.)

⊢ (A ∩
(B ∖ 𝐶)) = ((A ∩ B)
∖ 𝐶) 

Theorem  indif1 3155 
Bring an intersection in and out of a class difference. (Contributed by
Mario Carneiro, 15May2015.)

⊢ ((A ∖
𝐶) ∩ B) = ((A ∩
B) ∖ 𝐶) 

Theorem  indifcom 3156 
Commutation law for intersection and difference. (Contributed by Scott
Fenton, 18Feb2013.)

⊢ (A ∩
(B ∖ 𝐶)) = (B
∩ (A ∖ 𝐶)) 

Theorem  indi 3157 
Distributive law for intersection over union. Exercise 10 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30Sep2002.) (Proof
shortened by Andrew Salmon, 26Jun2011.)

⊢ (A ∩
(B ∪ 𝐶)) = ((A ∩ B)
∪ (A ∩ 𝐶)) 

Theorem  undi 3158 
Distributive law for union over intersection. Exercise 11 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30Sep2002.) (Proof
shortened by Andrew Salmon, 26Jun2011.)

⊢ (A ∪
(B ∩ 𝐶)) = ((A ∪ B)
∩ (A ∪ 𝐶)) 

Theorem  indir 3159 
Distributive law for intersection over union. Theorem 28 of [Suppes]
p. 27. (Contributed by NM, 30Sep2002.)

⊢ ((A ∪
B) ∩ 𝐶) = ((A
∩ 𝐶) ∪ (B ∩ 𝐶)) 

Theorem  undir 3160 
Distributive law for union over intersection. Theorem 29 of [Suppes]
p. 27. (Contributed by NM, 30Sep2002.)

⊢ ((A ∩
B) ∪ 𝐶) = ((A
∪ 𝐶) ∩ (B ∪ 𝐶)) 

Theorem  uneqin 3161 
Equality of union and intersection implies equality of their arguments.
(Contributed by NM, 16Apr2006.) (Proof shortened by Andrew Salmon,
26Jun2011.)

⊢ ((A ∪
B) = (A ∩ B)
↔ A = B) 

Theorem  difundi 3162 
Distributive law for class difference. Theorem 39 of [Suppes] p. 29.
(Contributed by NM, 17Aug2004.)

⊢ (A ∖
(B ∪ 𝐶)) = ((A ∖ B)
∩ (A ∖ 𝐶)) 

Theorem  difundir 3163 
Distributive law for class difference. (Contributed by NM,
17Aug2004.)

⊢ ((A ∪
B) ∖ 𝐶) = ((A
∖ 𝐶) ∪ (B ∖ 𝐶)) 

Theorem  difindiss 3164 
Distributive law for class difference. In classical logic, for example,
theorem 40 of [Suppes] p. 29, this is an
equality instead of subset.
(Contributed by Jim Kingdon, 26Jul2018.)

⊢ ((A ∖
B) ∪ (A ∖ 𝐶)) ⊆ (A ∖ (B
∩ 𝐶)) 

Theorem  difindir 3165 
Distributive law for class difference. (Contributed by NM,
17Aug2004.)

⊢ ((A ∩
B) ∖ 𝐶) = ((A
∖ 𝐶) ∩ (B ∖ 𝐶)) 

Theorem  indifdir 3166 
Distribute intersection over difference. (Contributed by Scott Fenton,
14Apr2011.)

⊢ ((A ∖
B) ∩ 𝐶) = ((A
∩ 𝐶) ∖ (B ∩ 𝐶)) 

Theorem  difdif2ss 3167 
Set difference with a set difference. In classical logic this would be
equality rather than subset. (Contributed by Jim Kingdon,
27Jul2018.)

⊢ ((A ∖
B) ∪ (A ∩ 𝐶)) ⊆ (A ∖ (B
∖ 𝐶)) 

Theorem  undm 3168 
De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19.
(Contributed by NM, 18Aug2004.)

⊢ (V ∖ (A ∪ B)) =
((V ∖ A) ∩ (V ∖ B)) 

Theorem  indmss 3169 
De Morgan's law for intersection. In classical logic, this would be
equality rather than subset, as in Theorem 5.2(13') of [Stoll] p. 19.
(Contributed by Jim Kingdon, 27Jul2018.)

⊢ ((V ∖ A) ∪ (V ∖ B)) ⊆ (V ∖ (A ∩ B)) 

Theorem  difun1 3170 
A relationship involving double difference and union. (Contributed by NM,
29Aug2004.)

⊢ (A ∖
(B ∪ 𝐶)) = ((A ∖ B)
∖ 𝐶) 

Theorem  undif3ss 3171 
A subset relationship involving class union and class difference. In
classical logic, this would be equality rather than subset, as in the
first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by
Jim Kingdon, 28Jul2018.)

⊢ (A ∪
(B ∖ 𝐶)) ⊆ ((A ∪ B)
∖ (𝐶 ∖
A)) 

Theorem  difin2 3172 
Represent a set difference as an intersection with a larger difference.
(Contributed by Jeff Madsen, 2Sep2009.)

⊢ (A ⊆
𝐶 → (A ∖ B) =
((𝐶 ∖ B) ∩ A)) 

Theorem  dif32 3173 
Swap second and third argument of double difference. (Contributed by NM,
18Aug2004.)

⊢ ((A ∖
B) ∖ 𝐶) = ((A
∖ 𝐶) ∖
B) 

Theorem  difabs 3174 
Absorptionlike law for class difference: you can remove a class only
once. (Contributed by FL, 2Aug2009.)

⊢ ((A ∖
B) ∖ B) = (A ∖
B) 

Theorem  symdif1 3175 
Two ways to express symmetric difference. This theorem shows the
equivalence of the definition of symmetric difference in [Stoll] p. 13 and
the restated definition in Example 4.1 of [Stoll] p. 262. (Contributed by
NM, 17Aug2004.)

⊢ ((A ∖
B) ∪ (B ∖ A)) =
((A ∪ B) ∖ (A
∩ B)) 

2.1.13.5 Class abstractions with difference,
union, and intersection of two classes


Theorem  symdifxor 3176* 
Expressing symmetric difference with exclusiveor or two differences.
(Contributed by Jim Kingdon, 28Jul2018.)

⊢ ((A ∖
B) ∪ (B ∖ A)) =
{x ∣ (x ∈ A ⊻ x
∈ B)} 

Theorem  unab 3177 
Union of two class abstractions. (Contributed by NM, 29Sep2002.)
(Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ({x ∣
φ} ∪ {x ∣ ψ}) = {x
∣ (φ
∨ ψ)} 

Theorem  inab 3178 
Intersection of two class abstractions. (Contributed by NM,
29Sep2002.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ({x ∣
φ} ∩ {x ∣ ψ}) = {x
∣ (φ ∧ ψ)} 

Theorem  difab 3179 
Difference of two class abstractions. (Contributed by NM,
23Oct2004.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ({x ∣
φ} ∖ {x ∣ ψ}) = {x
∣ (φ ∧ ¬ ψ)} 

Theorem  notab 3180 
A class builder defined by a negation. (Contributed by FL,
18Sep2010.)

⊢ {x ∣
¬ φ} = (V ∖ {x ∣ φ}) 

Theorem  unrab 3181 
Union of two restricted class abstractions. (Contributed by NM,
25Mar2004.)

⊢ ({x ∈ A ∣
φ} ∪ {x ∈ A ∣ ψ}) = {x
∈ A
∣ (φ
∨ ψ)} 

Theorem  inrab 3182 
Intersection of two restricted class abstractions. (Contributed by NM,
1Sep2006.)

⊢ ({x ∈ A ∣
φ} ∩ {x ∈ A ∣ ψ}) = {x
∈ A
∣ (φ ∧ ψ)} 

Theorem  inrab2 3183* 
Intersection with a restricted class abstraction. (Contributed by NM,
19Nov2007.)

⊢ ({x ∈ A ∣
φ} ∩ B) = {x ∈ (A ∩
B) ∣ φ} 

Theorem  difrab 3184 
Difference of two restricted class abstractions. (Contributed by NM,
23Oct2004.)

⊢ ({x ∈ A ∣
φ} ∖ {x ∈ A ∣ ψ}) = {x
∈ A
∣ (φ ∧ ¬ ψ)} 

Theorem  dfrab2 3185* 
Alternate definition of restricted class abstraction. (Contributed by
NM, 20Sep2003.)

⊢ {x ∈ A ∣
φ} = ({x ∣ φ} ∩ A) 

Theorem  dfrab3 3186* 
Alternate definition of restricted class abstraction. (Contributed by
Mario Carneiro, 8Sep2013.)

⊢ {x ∈ A ∣
φ} = (A ∩ {x
∣ φ}) 

Theorem  notrab 3187* 
Complementation of restricted class abstractions. (Contributed by Mario
Carneiro, 3Sep2015.)

⊢ (A ∖
{x ∈
A ∣ φ}) = {x
∈ A
∣ ¬ φ} 

Theorem  dfrab3ss 3188* 
Restricted class abstraction with a common superset. (Contributed by
Stefan O'Rear, 12Sep2015.) (Proof shortened by Mario Carneiro,
8Nov2015.)

⊢ (A ⊆
B → {x ∈ A ∣ φ} = (A
∩ {x ∈ B ∣
φ})) 

Theorem  rabun2 3189 
Abstraction restricted to a union. (Contributed by Stefan O'Rear,
5Feb2015.)

⊢ {x ∈ (A ∪
B) ∣ φ} = ({x
∈ A
∣ φ} ∪ {x ∈ B ∣ φ}) 

2.1.13.6 Restricted uniqueness with difference,
union, and intersection


Theorem  reuss2 3190* 
Transfer uniqueness to a smaller subclass. (Contributed by NM,
20Oct2005.)

⊢ (((A
⊆ B ∧ ∀x ∈ A (φ →
ψ)) ∧
(∃x
∈ A
φ ∧
∃!x
∈ B
ψ)) → ∃!x ∈ A φ) 

Theorem  reuss 3191* 
Transfer uniqueness to a smaller subclass. (Contributed by NM,
21Aug1999.)

⊢ ((A ⊆
B ∧ ∃x ∈ A φ ∧ ∃!x ∈ B φ) → ∃!x ∈ A φ) 

Theorem  reuun1 3192* 
Transfer uniqueness to a smaller class. (Contributed by NM,
21Oct2005.)

⊢ ((∃x ∈ A φ ∧ ∃!x ∈ (A ∪ B)(φ ∨ ψ))
→ ∃!x ∈ A φ) 

Theorem  reuun2 3193* 
Transfer uniqueness to a smaller or larger class. (Contributed by NM,
21Oct2005.)

⊢ (¬ ∃x ∈ B φ → (∃!x ∈ (A ∪
B)φ ↔ ∃!x ∈ A φ)) 

Theorem  reupick 3194* 
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
NM, 21Aug1999.)

⊢ (((A
⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) ∧ φ) →
(x ∈
A ↔ x ∈ B)) 

Theorem  reupick3 3195* 
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 19Nov2016.)

⊢ ((∃!x ∈ A φ ∧ ∃x ∈ A (φ ∧ ψ) ∧ x ∈ A) →
(φ → ψ)) 

Theorem  reupick2 3196* 
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 15Dec2013.) (Proof shortened by Mario Carneiro,
19Nov2016.)

⊢ (((∀x ∈ A (ψ → φ) ∧ ∃x ∈ A ψ ∧ ∃!x ∈ A φ) ∧
x ∈
A) → (φ ↔ ψ)) 

2.1.14 The empty set


Syntax  c0 3197 
Extend class notation to include the empty set.

class ∅ 

Definition  dfnul 3198 
Define the empty set. Special case of Exercise 4.10(o) of [Mendelson]
p. 231. For a more traditional definition, but requiring a dummy
variable, see dfnul2 3199. (Contributed by NM, 5Aug1993.)

⊢ ∅ = (V ∖ V) 

Theorem  dfnul2 3199 
Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring]
p. 20. (Contributed by NM, 26Dec1996.)

⊢ ∅ = {x ∣ ¬ x = x} 

Theorem  dfnul3 3200 
Alternate definition of the empty set. (Contributed by NM,
25Mar2004.)

⊢ ∅ = {x ∈ A ∣ ¬ x ∈ A} 