Metamath Proof Explorer

Theorem emptyal

Description: On the empty domain, any universally quantified formula is true. (Contributed by Wolf Lammen, 12-Mar-2023)

Ref Expression
Assertion emptyal 
|- ( -. E. x T. -> A. x ph )

Proof

Step Hyp Ref Expression
1 emptyex 
 |-  ( -. E. x T. -> -. E. x -. ph )
2 alex 
 |-  ( A. x ph <-> -. E. x -. ph )
3 1 2 sylibr 
 |-  ( -. E. x T. -> A. x ph )