Theorem excom 1599

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 1598	. 2 |- ( E. x E. y ph -> E. y E. x ph )
2		excomim 1598	. 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 1426

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 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-ial 1472

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  excom13  1624  exrot3  1625  ee4anv  1857  sbexyz  1927  2exsb  1933  2euex  2035  2exeu  2040  2eu4  2041  rexcomf  2529  gencbvex  2665  euxfr2dc  2800  euind  2802  sbccomlem  2913  opelopabsbALT  4084  uniuni  4271  elvvv  4497  elco  4598  dmuni  4642  dm0rn0  4649  dmmrnm  4651  dmcosseq  4700  elres  4743  rnco  4932  coass  4944  oprabid  5673  dfoprab2  5688  opabex3d  5884  opabex3  5885  cnvoprab  5991  domen  6458  xpassen  6536  prarloc  7052  fisumcom2  10819