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
Unicode
Theorem
ral0
Description:
Vacuous universal quantification is always true.
(Contributed by
NM
, 20-Oct-2005)
Ref
Expression
Assertion
ral0
⊢
∀
x
∈
∅
φ
Proof
Step
Hyp
Ref
Expression
1
noel
⊢
¬
x
∈
∅
2
1
pm2.21i
⊢
x
∈
∅
→
φ
3
2
rgen
⊢
∀
x
∈
∅
φ