Theorem excom 1554

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

Syntax hints:   <-> wb 98   E.wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-ial 1427

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  excom13  1579  exrot3  1580  ee4anv  1809  sbexyz  1879  2exsb  1885  2euex  1987  2exeu  1992  2eu4  1993  rexcomf  2472  gencbvex  2600  euxfr2dc  2726  euind  2728  sbccomlem  2832  opelopabsbALT  3996  uniuni  4183  elvvv  4403  dmuni  4545  dm0rn0  4552  dmmrnm  4554  dmcosseq  4603  elres  4646  rnco  4827  coass  4839  oprabid  5537  dfoprab2  5552  opabex3d  5748  opabex3  5749  domen  6232  xpassen  6304  prarloc  6601