Metamath Proof Explorer

Theorem alexn

Description: A relationship between two quantifiers and negation. (Contributed by NM, 18-Aug-1993)

Ref Expression
Assertion alexn 
|- ( A. x E. y -. ph <-> -. E. x A. y ph )

Proof

Step Hyp Ref Expression
1 exnal 
 |-  ( E. y -. ph <-> -. A. y ph )
2 1 albii 
 |-  ( A. x E. y -. ph <-> A. x -. A. y ph )
3 alnex 
 |-  ( A. x -. A. y ph <-> -. E. x A. y ph )
4 2 3 bitri 
 |-  ( A. x E. y -. ph <-> -. E. x A. y ph )