Theorem excom 1664

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem excom

Step	Hyp	Ref	Expression
1		excomim 1663	. 2 |- ( E. x E. y ph -> E. y E. x ph )
2		excomim 1663	. 2 |- ( E. y E. x ph -> E. x E. y ph )
3	1, 2	impbii 126	1 |- ( E. x E. y ph <-> E. y E. x ph )

Syntax hints:   <-> wb 105   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excom13  1689  exrot3  1690  ee4anv  1934  sbexyz  2003  2exsb  2009  2euex  2113  2exeu  2118  2eu4  2119  rexcomf  2639  gencbvex  2784  euxfr2dc  2923  euind  2925  sbccomlem  3038  opelopabsbALT  4260  uniuni  4452  elvvv  4690  elco  4794  dmuni  4838  dm0rn0  4845  dmmrnm  4847  dmcosseq  4899  elres  4944  rnco  5136  coass  5148  oprabid  5907  dfoprab2  5922  opabex3d  6122  opabex3  6123  cnvoprab  6235  domen  6751  xpassen  6830  prarloc  7502  fisumcom2  11446  fprodcom2fi  11634