Theorem excom 1594

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 1593	. 2 |- ( E. x E. y ph -> E. y E. x ph )
2		excomim 1593	. 2 |- ( E. y E. x ph -> E. x E. y ph )
3	1, 2	impbii 124	1 |- ( E. x E. y ph <-> E. y E. x ph )

Syntax hints:   <-> wb 103   E.wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-ial 1467

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  excom13  1619  exrot3  1620  ee4anv  1850  sbexyz  1920  2exsb  1926  2euex  2028  2exeu  2033  2eu4  2034  rexcomf  2516  gencbvex  2645  euxfr2dc  2777  euind  2779  sbccomlem  2888  opelopabsbALT  4014  uniuni  4201  elvvv  4421  dmuni  4563  dm0rn0  4570  dmmrnm  4572  dmcosseq  4621  elres  4664  rnco  4847  coass  4859  oprabid  5557  dfoprab2  5572  opabex3d  5768  opabex3  5769  cnvoprab  5875  domen  6255  xpassen  6327  prarloc  6693