Theorem excom 1623

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-ial 1495

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excom13  1648  exrot3  1649  ee4anv  1882  sbexyz  1952  2exsb  1958  2euex  2060  2exeu  2065  2eu4  2066  rexcomf  2565  gencbvex  2701  euxfr2dc  2836  euind  2838  sbccomlem  2949  opelopabsbALT  4139  uniuni  4330  elvvv  4560  elco  4663  dmuni  4707  dm0rn0  4714  dmmrnm  4716  dmcosseq  4766  elres  4811  rnco  5001  coass  5013  oprabid  5755  dfoprab2  5770  opabex3d  5971  opabex3  5972  cnvoprab  6083  domen  6597  xpassen  6675  prarloc  7253  fisumcom2  11093