Theorem excom 1393

Description: Theorem 19.11 of [Margaris] p. 89.

Assertion

Ref	Expression
excom	|- (E.xE.yph <-> E.yE.xph)

Proof of Theorem excom

Step	Hyp	Ref	Expression
1		excomim 1392	. 2 |- (E.xE.yph -> E.yE.xph)
2		excomim 1392	. 2 |- (E.yE.xph -> E.xE.yph)
3	1, 2	impbii 174	1 |- (E.xE.yph <-> E.yE.xph)

Syntax hints:   <-> wb 163  E.wex 1326

This theorem is referenced by:  excom13 1452  exrot3 1453  ee4anv 1710  2exsb 1742  2euex 1844  2euexOLD 1845  2exeu 1850  2eu1 1853  2eu4 1856  rexcom 2243  gencbvex 2334  gencbvexOLD 2335  euind 2439  sbccomglem 2525  dfiun2gOLD 3284  iunn0OLD 3316  opabidOLD 3558  opelopabsb 3564  uniuni 3806  elvvv 4054  dmuni 4166  dm0rn0 4175  dmcossOLD 4212  dmcosseq 4214  dmcosseqOLD 4215  rnuni 4327  rnco 4404  coass 4415  imaiun 4840  dfoprab2 4917  iinon 5115  domen 5438  xpcomen 5498  xpassen 5500  scott0 5847  aceq5lem1 5897  aceq5lem4 5900  cflem 6053  genpass 6264  addcompr 6275  mulcompr 6277  ltexprlem1 6294  ltexprlem4 6297  reclem1pr 6308  reclem2pr 6309  suplem1pr 6313  oprabopabf 10157  extbas1 10291  elres 13824  frxp 13951  rcfpfillem3 14930  opabex3 15701  prtlem16 16272  pm11.6 16349

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain