Metamath Proof Explorer

Theorem empty

Description: Two characterizations of the empty domain. (Contributed by Gérard Lang, 5-Feb-2024)

Ref Expression
Assertion empty 
|- ( -. E. x T. <-> A. x F. )

Proof

Step Hyp Ref Expression
1 df-fal 
 |-  ( F. <-> -. T. )
2 1 albii 
 |-  ( A. x F. <-> A. x -. T. )
3 alnex 
 |-  ( A. x -. T. <-> -. E. x T. )
4 2 3 bitr2i 
 |-  ( -. E. x T. <-> A. x F. )