Type  Label  Description 
Statement 

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

⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 

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

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶)) 

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

⊢ 𝐴 ⊆ 𝐵
& ⊢ 𝐴 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶) 

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

⊢ (𝜑 → 𝐴 ⊆ 𝐵)
& ⊢ (𝜑 → 𝐴 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶)) 

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

⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) 

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

⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) 

Theorem  ssrind 3307 
Add right intersection to subclass relation. (Contributed by Glauco
Siliprandi, 2Jan2022.)

⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) 

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

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) 

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

⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶) 

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

⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶) 

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


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

⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴 

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

⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴 

Theorem  dfss4st 3313* 
Subclass defined in terms of class difference. (Contributed by NM,
22Mar1998.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (∀𝑥STAB 𝑥 ∈ 𝐴 → (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴)) 

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

⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ (𝐵 ∖ (𝐵 ∖ 𝐴))) 

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

⊢ (𝐴 ∪ 𝐵) ⊆ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) 

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

⊢ (𝐴 ∩ 𝐵) ⊆ (𝐴 ∖ (V ∖ 𝐵)) 

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

⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) 

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

⊢ 𝐴 ⊆ (V ∖ (V ∖ 𝐴)) 

Theorem  unssin 3319 
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.)

⊢ (𝐴 ∪ 𝐵) ⊆ (V ∖ ((V ∖ 𝐴) ∩ (V ∖ 𝐵))) 

Theorem  inssun 3320 
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.)

⊢ (𝐴 ∩ 𝐵) ⊆ (V ∖ ((V ∖ 𝐴) ∪ (V ∖ 𝐵))) 

Theorem  inssddif 3321 
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.)

⊢ (𝐴 ∩ 𝐵) ⊆ (𝐴 ∖ (𝐴 ∖ 𝐵)) 

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

⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) 

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

⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵) 

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

⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) 

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

⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶) 

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

⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶)) 

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

⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) 

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

⊢ (𝐴 ∪ (𝐵 ∩ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ 𝐶)) 

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

⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) 

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

⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶)) 

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

⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) ↔ 𝐴 = 𝐵) 

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

⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶)) 

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

⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) 

Theorem  difindiss 3334 
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.)

⊢ ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) ⊆ (𝐴 ∖ (𝐵 ∩ 𝐶)) 

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

⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶)) 

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

⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶)) 

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

⊢ ((𝐴 ∖ 𝐵) ∪ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∖ (𝐵 ∖ 𝐶)) 

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

⊢ (V ∖ (𝐴 ∪ 𝐵)) = ((V ∖ 𝐴) ∩ (V ∖ 𝐵)) 

Theorem  indmss 3339 
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 ∖ 𝐴) ∪ (V ∖ 𝐵)) ⊆ (V ∖ (𝐴 ∩ 𝐵)) 

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

⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶) 

Theorem  undif3ss 3341 
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.)

⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) ⊆ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) 

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

⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴)) 

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

⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵) 

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

⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) 

Theorem  symdif1 3345 
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.)

⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) = ((𝐴 ∪ 𝐵) ∖ (𝐴 ∩ 𝐵)) 

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


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

⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)} 

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

⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)} 

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

⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)} 

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

⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)} 

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

⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑}) 

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

⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} 

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

⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} 

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

⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑} 

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

⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)} 

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

⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴) 

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

⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑}) 

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

⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} 

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

⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑})) 

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

⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝜑} = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜑}) 

2.1.13.6 Restricted uniqueness with difference,
union, and intersection


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

⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) 

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

⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑) 

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

⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) 

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

⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑)) 

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

⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) 

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

⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓)) 

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

⊢ (((∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓)) 

2.1.14 The empty set


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

class ∅ 

Definition  dfnul 3368 
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 3369. (Contributed by NM, 5Aug1993.)

⊢ ∅ = (V ∖ V) 

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

⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} 

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

⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} 

Theorem  noel 3371 
The empty set has no elements. Theorem 6.14 of [Quine] p. 44.
(Contributed by NM, 5Aug1993.) (Proof shortened by Mario Carneiro,
1Sep2015.)

⊢ ¬ 𝐴 ∈ ∅ 

Theorem  n0i 3372 
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2705. (Contributed by NM, 31Dec1993.)

⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) 

Theorem  ne0i 3373 
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2705. (Contributed by NM, 31Dec1993.)

⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) 

Theorem  ne0d 3374 
Deduction form of ne0i 3373. If a class has elements, then it is
nonempty. (Contributed by Glauco Siliprandi, 23Oct2021.)

⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) 

Theorem  n0ii 3375 
If a class has elements, then it is not empty. Inference associated
with n0i 3372. (Contributed by BJ, 15Jul2021.)

⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ¬ 𝐵 = ∅ 

Theorem  ne0ii 3376 
If a class has elements, then it is nonempty. Inference associated with
ne0i 3373. (Contributed by Glauco Siliprandi,
11Dec2019.)

⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐵 ≠ ∅ 

Theorem  vn0 3377 
The universal class is not equal to the empty set. (Contributed by NM,
11Sep2008.)

⊢ V ≠ ∅ 

Theorem  vn0m 3378 
The universal class is inhabited. (Contributed by Jim Kingdon,
17Dec2018.)

⊢ ∃𝑥 𝑥 ∈ V 

Theorem  n0rf 3379 
An inhabited class is nonempty. Following the Definition of [Bauer],
p. 483, we call a class 𝐴 nonempty if 𝐴 ≠ ∅ and
inhabited if
it has at least one element. In classical logic these two concepts are
equivalent, for example see Proposition 5.17(1) of [TakeutiZaring]
p. 20. This version of n0r 3380 requires only that 𝑥 not be free in,
rather than not occur in, 𝐴. (Contributed by Jim Kingdon,
31Jul2018.)

⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) 

Theorem  n0r 3380* 
An inhabited class is nonempty. See n0rf 3379 for more discussion.
(Contributed by Jim Kingdon, 31Jul2018.)

⊢ (∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) 

Theorem  neq0r 3381* 
An inhabited class is nonempty. See n0rf 3379 for more discussion.
(Contributed by Jim Kingdon, 31Jul2018.)

⊢ (∃𝑥 𝑥 ∈ 𝐴 → ¬ 𝐴 = ∅) 

Theorem  reximdva0m 3382* 
Restricted existence deduced from inhabited class. (Contributed by Jim
Kingdon, 31Jul2018.)

⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ ((𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 𝜓) 

Theorem  n0mmoeu 3383* 
A case of equivalence of "at most one" and "only one". If
a class is
inhabited, that class having at most one element is equivalent to it
having only one element. (Contributed by Jim Kingdon, 31Jul2018.)

⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 𝑥 ∈ 𝐴)) 

Theorem  rex0 3384 
Vacuous existential quantification is false. (Contributed by NM,
15Oct2003.)

⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 

Theorem  eq0 3385* 
The empty set has no elements. Theorem 2 of [Suppes] p. 22.
(Contributed by NM, 29Aug1993.)

⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) 

Theorem  eqv 3386* 
The universe contains every set. (Contributed by NM, 11Sep2006.)

⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴) 

Theorem  notm0 3387* 
A class is not inhabited if and only if it is empty. (Contributed by
Jim Kingdon, 1Jul2022.)

⊢ (¬ ∃𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅) 

Theorem  nel0 3388* 
From the general negation of membership in 𝐴, infer that 𝐴 is
the empty set. (Contributed by BJ, 6Oct2018.)

⊢ ¬ 𝑥 ∈ 𝐴 ⇒ ⊢ 𝐴 = ∅ 

Theorem  0el 3389* 
Membership of the empty set in another class. (Contributed by NM,
29Jun2004.)

⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥) 

Theorem  abvor0dc 3390* 
The class builder of a decidable proposition not containing the
abstraction variable is either the universal class or the empty set.
(Contributed by Jim Kingdon, 1Aug2018.)

⊢ (DECID 𝜑 → ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅)) 

Theorem  abn0r 3391 
Nonempty class abstraction. (Contributed by Jim Kingdon, 1Aug2018.)

⊢ (∃𝑥𝜑 → {𝑥 ∣ 𝜑} ≠ ∅) 

Theorem  abn0m 3392* 
Inhabited class abstraction. (Contributed by Jim Kingdon,
8Jul2022.)

⊢ (∃𝑦 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥𝜑) 

Theorem  rabn0r 3393 
Nonempty restricted class abstraction. (Contributed by Jim Kingdon,
1Aug2018.)

⊢ (∃𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅) 

Theorem  rabn0m 3394* 
Inhabited restricted class abstraction. (Contributed by Jim Kingdon,
18Sep2018.)

⊢ (∃𝑦 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐴 𝜑) 

Theorem  rab0 3395 
Any restricted class abstraction restricted to the empty set is empty.
(Contributed by NM, 15Oct2003.) (Proof shortened by Andrew Salmon,
26Jun2011.)

⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅ 

Theorem  rabeq0 3396 
Condition for a restricted class abstraction to be empty. (Contributed
by Jeff Madsen, 7Jun2010.)

⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) 

Theorem  abeq0 3397 
Condition for a class abstraction to be empty. (Contributed by Jim
Kingdon, 12Aug2018.)

⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) 

Theorem  rabxmdc 3398* 
Law of excluded middle given decidability, in terms of restricted class
abstractions. (Contributed by Jim Kingdon, 2Aug2018.)

⊢ (∀𝑥DECID 𝜑 → 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑})) 

Theorem  rabnc 3399* 
Law of noncontradiction, in terms of restricted class abstractions.
(Contributed by Jeff Madsen, 20Jun2011.)

⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅ 

Theorem  un0 3400 
The union of a class with the empty set is itself. Theorem 24 of
[Suppes] p. 27. (Contributed by NM,
5Aug1993.)

⊢ (𝐴 ∪ ∅) = 𝐴 