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  4305  uniuni  4498  elvvv  4738  elco  4844  dmuni  4888  dm0rn0  4895  dmmrnm  4897  dmcosseq  4950  elres  4995  rnco  5189  coass  5201  oprabid  5976  dfoprab2  5992  opabex3d  6206  opabex3  6207  cnvoprab  6320  domen  6840  xpassen  6925  prarloc  7616  fisumcom2  11749  fprodcom2fi  11937