Theorem excom 1687

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

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excom13  1712  exrot3  1713  ee4anv  1962  sbexyz  2031  2exsb  2037  2euex  2141  2exeu  2146  2eu4  2147  rexcomf  2668  gencbvex  2819  euxfr2dc  2958  euind  2960  sbccomlem  3073  opelopabsbALT  4306  uniuni  4499  elvvv  4739  elco  4845  dmuni  4889  dm0rn0  4896  dmmrnm  4898  dmcosseq  4951  elres  4996  rnco  5190  coass  5202  oprabid  5978  dfoprab2  5994  opabex3d  6208  opabex3  6209  cnvoprab  6322  domen  6842  xpassen  6927  prarloc  7618  fisumcom2  11782  fprodcom2fi  11970