Theorem excom 1644

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

Syntax hints:   <-> wb 104   E.wex 1472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excom13  1669  exrot3  1670  ee4anv  1914  sbexyz  1983  2exsb  1989  2euex  2093  2exeu  2098  2eu4  2099  rexcomf  2619  gencbvex  2758  euxfr2dc  2897  euind  2899  sbccomlem  3011  opelopabsbALT  4219  uniuni  4410  elvvv  4648  elco  4751  dmuni  4795  dm0rn0  4802  dmmrnm  4804  dmcosseq  4856  elres  4901  rnco  5091  coass  5103  oprabid  5850  dfoprab2  5865  opabex3d  6066  opabex3  6067  cnvoprab  6178  domen  6693  xpassen  6772  prarloc  7417  fisumcom2  11328  fprodcom2fi  11516