Metamath Proof Explorer

Theorem ral0

Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005)

Ref Expression
Assertion ral0 
|- A. x e. (/) ph

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. x e. (/)
2 1 pm2.21i 
 |-  ( x e. (/) -> ph )
3 2 rgen 
 |-  A. x e. (/) ph