Metamath Proof Explorer

Theorem ral0

Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005) Avoid df-clel , ax-8 . (Revised by GG, 2-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  (/) = (/)
2 rzal 
 |-  ( (/) = (/) -> A. x e. (/) ph )
3 1 2 ax-mp 
 |-  A. x e. (/) ph