Metamath Proof Explorer

Theorem excom

Description: Theorem 19.11 of Margaris p. 89. (Contributed by NM, 5-Aug-1993) Remove dependencies on ax-5 , ax-6 , ax-7 , ax-10 , ax-12 . (Revised by Wolf Lammen, 8-Jan-2018) (Proof shortened by Wolf Lammen, 22-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 alcom 
 |-  ( A. x A. y -. ph <-> A. y A. x -. ph )
2 1 notbii 
 |-  ( -. A. x A. y -. ph <-> -. A. y A. x -. ph )
3 2exnaln 
 |-  ( E. x E. y ph <-> -. A. x A. y -. ph )
4 2exnaln 
 |-  ( E. y E. x ph <-> -. A. y A. x -. ph )
5 2 3 4 3bitr4i 
 |-  ( E. x E. y ph <-> E. y E. x ph )