Type  Label  Description 
Statement 

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

⊢ ¬ A
∈ ∅ 

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

⊢ (B ∈ A →
¬ A = ∅) 

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

⊢ (B ∈ A →
A ≠ ∅) 

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

⊢ V ≠ ∅ 

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

⊢ ∃x x ∈ V 

Theorem  n0rf 3206 
An inhabited class is nonempty. Following the Definition of [Bauer],
p. 483, we call a class A nonempty if A ≠ ∅ 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 3207 requires only that x not be free in,
rather than not occur in, A. (Contributed by Jim Kingdon,
31Jul2018.)

⊢ ℲxA ⇒ ⊢ (∃x x ∈ A → A ≠
∅) 

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

⊢ (∃x x ∈ A →
A ≠ ∅) 

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

⊢ (∃x x ∈ A →
¬ A = ∅) 

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

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

Theorem  n0mmoeu 3210* 
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.)

⊢ (∃x x ∈ A →
(∃*x
x ∈
A ↔ ∃!x x ∈ A)) 

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

⊢ ¬ ∃x ∈ ∅ φ 

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

⊢ (A =
∅ ↔ ∀x ¬ x ∈ A) 

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

⊢ (A = V
↔ ∀x x ∈ A) 

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

⊢ (∅ ∈
A ↔ ∃x ∈ A ∀y ¬
y ∈
x) 

Theorem  abvor0dc 3215* 
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 φ → ({x ∣ φ} = V ∨
{x ∣ φ} = ∅)) 

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

⊢ (∃xφ →
{x ∣ φ} ≠ ∅) 

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

⊢ (∃x ∈ A φ →
{x ∈
A ∣ φ} ≠ ∅) 

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

⊢ (∃y y ∈ {x ∈ A ∣
φ} ↔ ∃x ∈ A φ) 

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

⊢ {x ∈ ∅ ∣ φ} = ∅ 

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

⊢ ({x ∈ A ∣
φ} = ∅ ↔ ∀x ∈ A ¬
φ) 

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

⊢ ({x ∣
φ} = ∅ ↔ ∀x ¬
φ) 

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

⊢ (∀xDECID φ → A = ({x ∈ A ∣
φ} ∪ {x ∈ A ∣ ¬ φ})) 

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

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

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

⊢ (A ∪
∅) = A 

Theorem  in0 3225 
The intersection of a class with the empty set is the empty set.
Theorem 16 of [Suppes] p. 26.
(Contributed by NM, 5Aug1993.)

⊢ (A ∩
∅) = ∅ 

Theorem  inv1 3226 
The intersection of a class with the universal class is itself. Exercise
4.10(k) of [Mendelson] p. 231.
(Contributed by NM, 17May1998.)

⊢ (A ∩ V)
= A 

Theorem  unv 3227 
The union of a class with the universal class is the universal class.
Exercise 4.10(l) of [Mendelson] p. 231.
(Contributed by NM,
17May1998.)

⊢ (A ∪ V)
= V 

Theorem  0ss 3228 
The null set is a subset of any class. Part of Exercise 1 of
[TakeutiZaring] p. 22.
(Contributed by NM, 5Aug1993.)

⊢ ∅ ⊆ A 

Theorem  ss0b 3229 
Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its
converse. (Contributed by NM, 17Sep2003.)

⊢ (A ⊆
∅ ↔ A =
∅) 

Theorem  ss0 3230 
Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23.
(Contributed by NM, 13Aug1994.)

⊢ (A ⊆
∅ → A =
∅) 

Theorem  sseq0 3231 
A subclass of an empty class is empty. (Contributed by NM, 7Mar2007.)
(Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ((A ⊆
B ∧
B = ∅) → A = ∅) 

Theorem  ssn0 3232 
A class with a nonempty subclass is nonempty. (Contributed by NM,
17Feb2007.)

⊢ ((A ⊆
B ∧
A ≠ ∅) → B ≠ ∅) 

Theorem  abf 3233 
A class builder with a false argument is empty. (Contributed by NM,
20Jan2012.)

⊢ ¬ φ ⇒ ⊢ {x ∣ φ} = ∅ 

Theorem  eq0rdv 3234* 
Deduction rule for equality to the empty set. (Contributed by NM,
11Jul2014.)

⊢ (φ
→ ¬ x ∈ A) ⇒ ⊢ (φ → A = ∅) 

Theorem  csbprc 3235 
The proper substitution of a proper class for a set into a class results
in the empty set. (Contributed by NM, 17Aug2018.)

⊢ (¬ A
∈ V → ⦋A / x⦌B = ∅) 

Theorem  un00 3236 
Two classes are empty iff their union is empty. (Contributed by NM,
11Aug2004.)

⊢ ((A =
∅ ∧ B = ∅) ↔ (A ∪ B) =
∅) 

Theorem  vss 3237 
Only the universal class has the universal class as a subclass.
(Contributed by NM, 17Sep2003.) (Proof shortened by Andrew Salmon,
26Jun2011.)

⊢ (V ⊆ A ↔ A =
V) 

Theorem  0pss 3238 
The null set is a proper subset of any nonempty set. (Contributed by NM,
27Feb1996.)

⊢ (∅ ⊊ A ↔ A ≠
∅) 

Theorem  npss0 3239 
No set is a proper subset of the empty set. (Contributed by NM,
17Jun1998.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ¬ A
⊊ ∅ 

Theorem  pssv 3240 
Any nonuniversal class is a proper subclass of the universal class.
(Contributed by NM, 17May1998.)

⊢ (A ⊊
V ↔ ¬ A = V) 

Theorem  disj 3241* 
Two ways of saying that two classes are disjoint (have no members in
common). (Contributed by NM, 17Feb2004.)

⊢ ((A ∩
B) = ∅ ↔ ∀x ∈ A ¬
x ∈
B) 

Theorem  disjr 3242* 
Two ways of saying that two classes are disjoint. (Contributed by Jeff
Madsen, 19Jun2011.)

⊢ ((A ∩
B) = ∅ ↔ ∀x ∈ B ¬
x ∈
A) 

Theorem  disj1 3243* 
Two ways of saying that two classes are disjoint (have no members in
common). (Contributed by NM, 19Aug1993.)

⊢ ((A ∩
B) = ∅ ↔ ∀x(x ∈ A → ¬ x ∈ B)) 

Theorem  reldisj 3244 
Two ways of saying that two classes are disjoint, using the complement
of B
relative to a universe 𝐶. (Contributed by NM,
15Feb2007.) (Proof shortened by Andrew Salmon, 26Jun2011.)

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

Theorem  disj3 3245 
Two ways of saying that two classes are disjoint. (Contributed by NM,
19May1998.)

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

Theorem  disjne 3246 
Members of disjoint sets are not equal. (Contributed by NM,
28Mar2007.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (((A ∩
B) = ∅ ∧ 𝐶 ∈
A ∧ 𝐷 ∈ B) →
𝐶 ≠ 𝐷) 

Theorem  disjel 3247 
A set can't belong to both members of disjoint classes. (Contributed by
NM, 28Feb2015.)

⊢ (((A ∩
B) = ∅ ∧ 𝐶 ∈
A) → ¬ 𝐶 ∈
B) 

Theorem  disj2 3248 
Two ways of saying that two classes are disjoint. (Contributed by NM,
17May1998.)

⊢ ((A ∩
B) = ∅ ↔ A ⊆ (V ∖ B)) 

Theorem  disj4im 3249 
A consequence of two classes being disjoint. In classical logic this
would be a biconditional. (Contributed by Jim Kingdon, 2Aug2018.)

⊢ ((A ∩
B) = ∅ → ¬ (A ∖ B)
⊊ A) 

Theorem  ssdisj 3250 
Intersection with a subclass of a disjoint class. (Contributed by FL,
24Jan2007.)

⊢ ((A ⊆
B ∧
(B ∩ 𝐶) = ∅) → (A ∩ 𝐶) = ∅) 

Theorem  disjpss 3251 
A class is a proper subset of its union with a disjoint nonempty class.
(Contributed by NM, 15Sep2004.)

⊢ (((A ∩
B) = ∅ ∧ B ≠
∅) → A ⊊ (A ∪ B)) 

Theorem  undisj1 3252 
The union of disjoint classes is disjoint. (Contributed by NM,
26Sep2004.)

⊢ (((A ∩
𝐶) = ∅ ∧ (B ∩
𝐶) = ∅) ↔
((A ∪ B) ∩ 𝐶) = ∅) 

Theorem  undisj2 3253 
The union of disjoint classes is disjoint. (Contributed by NM,
13Sep2004.)

⊢ (((A ∩
B) = ∅ ∧ (A ∩
𝐶) = ∅) ↔
(A ∩ (B ∪ 𝐶)) = ∅) 

Theorem  ssindif0im 3254 
Subclass implies empty intersection with difference from the universal
class. (Contributed by NM, 17Sep2003.)

⊢ (A ⊆
B → (A ∩ (V ∖ B)) = ∅) 

Theorem  inelcm 3255 
The intersection of classes with a common member is nonempty.
(Contributed by NM, 7Apr1994.)

⊢ ((A ∈ B ∧ A ∈ 𝐶) → (B ∩ 𝐶) ≠ ∅) 

Theorem  minel 3256 
A minimum element of a class has no elements in common with the class.
(Contributed by NM, 22Jun1994.)

⊢ ((A ∈ B ∧ (𝐶 ∩ B) = ∅) → ¬ A ∈ 𝐶) 

Theorem  undif4 3257 
Distribute union over difference. (Contributed by NM, 17May1998.)
(Proof shortened by Andrew Salmon, 26Jun2011.)

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

Theorem  disjssun 3258 
Subset relation for disjoint classes. (Contributed by NM,
25Oct2005.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ((A ∩
B) = ∅ → (A ⊆ (B
∪ 𝐶) ↔ A ⊆ 𝐶)) 

Theorem  ssdif0im 3259 
Subclass implies empty difference. One direction of Exercise 7 of
[TakeutiZaring] p. 22. In
classical logic this would be an
equivalence. (Contributed by Jim Kingdon, 2Aug2018.)

⊢ (A ⊆
B → (A ∖ B) =
∅) 

Theorem  vdif0im 3260 
Universal class equality in terms of empty difference. (Contributed by
Jim Kingdon, 3Aug2018.)

⊢ (A = V
→ (V ∖ A) =
∅) 

Theorem  difrab0eqim 3261* 
If the difference between the restricting class of a restricted class
abstraction and the restricted class abstraction is empty, the
restricting class is equal to this restricted class abstraction.
(Contributed by Jim Kingdon, 3Aug2018.)

⊢ (𝑉 = {x
∈ 𝑉 ∣ φ} → (𝑉 ∖ {x ∈ 𝑉 ∣ φ}) = ∅) 

Theorem  ssnelpss 3262 
A subclass missing a member is a proper subclass. (Contributed by NM,
12Jan2002.)

⊢ (A ⊆
B → ((𝐶 ∈
B ∧ ¬
𝐶 ∈ A) →
A ⊊ B)) 

Theorem  ssnelpssd 3263 
Subclass inclusion with one element of the superclass missing is proper
subclass inclusion. Deduction form of ssnelpss 3262. (Contributed by
David Moews, 1May2017.)

⊢ (φ
→ A ⊆ B)
& ⊢ (φ
→ 𝐶 ∈ B)
& ⊢ (φ
→ ¬ 𝐶 ∈ A) ⇒ ⊢ (φ → A ⊊ B) 

Theorem  inssdif0im 3264 
Intersection, subclass, and difference relationship. In classical logic
the converse would also hold. (Contributed by Jim Kingdon,
3Aug2018.)

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

Theorem  difid 3265 
The difference between a class and itself is the empty set. Proposition
5.15 of [TakeutiZaring] p. 20. Also
Theorem 32 of [Suppes] p. 28.
(Contributed by NM, 22Apr2004.)

⊢ (A ∖
A) = ∅ 

Theorem  difidALT 3266 
The difference between a class and itself is the empty set. Proposition
5.15 of [TakeutiZaring] p. 20.
Also Theorem 32 of [Suppes] p. 28.
Alternate proof of difid 3265. (Contributed by David Abernethy,
17Jun2012.) (Proof modification is discouraged.)
(New usage is discouraged.)

⊢ (A ∖
A) = ∅ 

Theorem  dif0 3267 
The difference between a class and the empty set. Part of Exercise 4.4 of
[Stoll] p. 16. (Contributed by NM,
17Aug2004.)

⊢ (A ∖
∅) = A 

Theorem  0dif 3268 
The difference between the empty set and a class. Part of Exercise 4.4 of
[Stoll] p. 16. (Contributed by NM,
17Aug2004.)

⊢ (∅ ∖ A) = ∅ 

Theorem  disjdif 3269 
A class and its relative complement are disjoint. Theorem 38 of [Suppes]
p. 29. (Contributed by NM, 24Mar1998.)

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

Theorem  difin0 3270 
The difference of a class from its intersection is empty. Theorem 37 of
[Suppes] p. 29. (Contributed by NM,
17Aug2004.) (Proof shortened by
Andrew Salmon, 26Jun2011.)

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

Theorem  undif1ss 3271 
Absorption of difference by union. In classical logic, as Theorem 35 of
[Suppes] p. 29, this would be equality
rather than subset. (Contributed
by Jim Kingdon, 4Aug2018.)

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

Theorem  undif2ss 3272 
Absorption of difference by union. In classical logic, as in Part of
proof of Corollary 6K of [Enderton] p.
144, this would be equality rather
than subset. (Contributed by Jim Kingdon, 4Aug2018.)

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

Theorem  undifabs 3273 
Absorption of difference by union. (Contributed by NM, 18Aug2013.)

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

Theorem  inundifss 3274 
The intersection and class difference of a class with another class are
contained in the original class. In classical logic we'd be able to make
a stronger statement: that everything in the original class is in the
intersection or the difference (that is, this theorem would be equality
rather than subset). (Contributed by Jim Kingdon, 4Aug2018.)

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

Theorem  difun2 3275 
Absorption of union by difference. Theorem 36 of [Suppes] p. 29.
(Contributed by NM, 19May1998.)

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

Theorem  undifss 3276 
Union of complementary parts into whole. (Contributed by Jim Kingdon,
4Aug2018.)

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

Theorem  ssdifin0 3277 
A subset of a difference does not intersect the subtrahend. (Contributed
by Jeff Hankins, 1Sep2013.) (Proof shortened by Mario Carneiro,
24Aug2015.)

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

Theorem  ssdifeq0 3278 
A class is a subclass of itself subtracted from another iff it is the
empty set. (Contributed by Steve Rodriguez, 20Nov2015.)

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

Theorem  ssundifim 3279 
A consequence of inclusion in the union of two classes. In classical
logic this would be a biconditional. (Contributed by Jim Kingdon,
4Aug2018.)

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

Theorem  difdifdirss 3280 
Distributive law for class difference. In classical logic, as in Exercise
4.8 of [Stoll] p. 16, this would be equality
rather than subset.
(Contributed by Jim Kingdon, 4Aug2018.)

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

Theorem  uneqdifeqim 3281 
Two ways that A and
B can
"partition" 𝐶 (when A and B
don't overlap and A is a part of 𝐶). In classical logic,
the
second implication would be a biconditional. (Contributed by Jim Kingdon,
4Aug2018.)

⊢ ((A ⊆
𝐶 ∧ (A ∩
B) = ∅) → ((A ∪ B) =
𝐶 → (𝐶 ∖ A) = B)) 

Theorem  r19.2m 3282* 
Theorem 19.2 of [Margaris] p. 89 with
restricted quantifiers (compare
19.2 1507). The restricted version is valid only when
the domain of
quantification is inhabited. (Contributed by Jim Kingdon,
5Aug2018.)

⊢ ((∃x x ∈ A ∧ ∀x ∈ A φ) →
∃x
∈ A
φ) 

Theorem  r19.3rmOLD 3283* 
Restricted quantification of wff not containing quantified variable.
This is a special case of r19.3rm 3285 where the two setvar variables are
both x, so
new proofs should just use r19.3rm 3285 instead.
(Contributed by Jim Kingdon, 5Aug2018.)
(New usage is discouraged.)

⊢ Ⅎxφ ⇒ ⊢ (∃x x ∈ A → (φ
↔ ∀x ∈ A φ)) 

Theorem  r19.28m 3284* 
Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It
is valid only when the domain of quantification is inhabited.
(Contributed by Jim Kingdon, 5Aug2018.)

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

Theorem  r19.3rm 3285* 
Restricted quantification of wff not containing quantified variable.
(Contributed by Jim Kingdon, 19Dec2018.)

⊢ Ⅎxφ ⇒ ⊢ (∃y y ∈ A → (φ
↔ ∀x ∈ A φ)) 

Theorem  r19.3rmv 3286* 
Restricted quantification of wff not containing quantified variable.
(Contributed by Jim Kingdon, 6Aug2018.)

⊢ (∃y y ∈ A →
(φ ↔ ∀x ∈ A φ)) 

Theorem  r19.9rmv 3287* 
Restricted quantification of wff not containing quantified variable.
(Contributed by Jim Kingdon, 5Aug2018.)

⊢ (∃y y ∈ A →
(φ ↔ ∃x ∈ A φ)) 

Theorem  r19.9rmvOLD 3288* 
Restricted quantification of wff not containing quantified variable.
This is a special case of r19.9rmv 3287 where x and y are the same
variable, but new proofs should use r19.9rmv 3287 instead.
(New usage is discouraged.) (Contributed by Jim Kingdon,
5Aug2018.)

⊢ (∃x x ∈ A →
(φ ↔ ∃x ∈ A φ)) 

Theorem  r19.28mv 3289* 
Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It
is valid only when the domain of quantification is inhabited.
(Contributed by Jim Kingdon, 6Aug2018.)

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

Theorem  r19.45mv 3290* 
Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed
by NM, 27May1998.)

⊢ (∃x x ∈ A →
(∃x
∈ A
(φ ∨
ψ) ↔ (φ ∨ ∃x ∈ A ψ))) 

Theorem  r19.27m 3291* 
Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It
is valid only when the domain of quantification is inhabited.
(Contributed by Jim Kingdon, 5Aug2018.)

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

Theorem  r19.27mv 3292* 
Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It
is valid only when the domain of quantification is inhabited.
(Contributed by Jim Kingdon, 5Aug2018.)

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

Theorem  rzal 3293* 
Vacuous quantification is always true. (Contributed by NM,
11Mar1997.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (A =
∅ → ∀x ∈ A φ) 

Theorem  rexn0 3294* 
Restricted existential quantification implies its restriction is
nonempty. (Contributed by Szymon Jaroszewicz, 3Apr2007.)

⊢ (∃x ∈ A φ →
A ≠ ∅) 

Theorem  rexm 3295* 
Restricted existential quantification implies its restriction is
inhabited. (Contributed by Jim Kingdon, 16Oct2018.)

⊢ (∃x ∈ A φ →
∃x
x ∈
A) 

Theorem  ralidm 3296* 
Idempotent law for restricted quantifier. (Contributed by NM,
28Mar1997.)

⊢ (∀x ∈ A ∀x ∈ A φ ↔
∀x
∈ A
φ) 

Theorem  ral0 3297 
Vacuous universal quantification is always true. (Contributed by NM,
20Oct2005.)

⊢ ∀x ∈ ∅ φ 

Theorem  rgenm 3298* 
Generalization rule that eliminates an inhabited class requirement.
(Contributed by Jim Kingdon, 5Aug2018.)

⊢ ((∃x x ∈ A ∧ x ∈ A) →
φ) ⇒ ⊢ ∀x ∈ A φ 

Theorem  ralf0 3299* 
The quantification of a falsehood is vacuous when true. (Contributed by
NM, 26Nov2005.)

⊢ ¬ φ ⇒ ⊢ (∀x ∈ A φ ↔ A = ∅) 

Theorem  ralm 3300 
Inhabited classes and restricted quantification. (Contributed by Jim
Kingdon, 6Aug2018.)

⊢ ((∃x x ∈ A →
∀x
∈ A
φ) ↔ ∀x ∈ A φ) 