Theorem excom 1642

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

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excom13  1667  exrot3  1668  ee4anv  1906  sbexyz  1978  2exsb  1984  2euex  2086  2exeu  2091  2eu4  2092  rexcomf  2593  gencbvex  2732  euxfr2dc  2869  euind  2871  sbccomlem  2983  opelopabsbALT  4181  uniuni  4372  elvvv  4602  elco  4705  dmuni  4749  dm0rn0  4756  dmmrnm  4758  dmcosseq  4810  elres  4855  rnco  5045  coass  5057  oprabid  5803  dfoprab2  5818  opabex3d  6019  opabex3  6020  cnvoprab  6131  domen  6645  xpassen  6724  prarloc  7311  fisumcom2  11207