Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The empty set
ral0
Next ⟩
ralf0
Metamath Proof Explorer
Ascii
Structured
Theorem
ral0
Description:
Vacuous universal quantification is always true.
(Contributed by
NM
, 20-Oct-2005)
Ref
Expression
Assertion
ral0
⊢
∀
𝑥
∈ ∅
𝜑
Proof
Step
Hyp
Ref
Expression
1
noel
⊢
¬
𝑥
∈ ∅
2
1
pm2.21i
⊢
(
𝑥
∈ ∅ →
𝜑
)
3
2
rgen
⊢
∀
𝑥
∈ ∅
𝜑