Theorem excom 1078

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 1077	. 2 |- (E.xE.yph -> E.yE.xph)
2		excomim 1077	. 2 |- (E.yE.xph -> E.xE.yph)
3	1, 2	impbii 155	1 |- (E.xE.yph <-> E.yE.xph)

Syntax hints:   <-> wb 144  E.wex 1012

This theorem is referenced by:  excom13 1130  exrot3 1131  ee4anv 1358  2exsb 1384  2euex 1475  2exeu 1480  2eu1 1483  2eu4 1486  rexcom 1813  gencbvex 1876  sbccomglem 2030  dfiun2g 2635  iunn0 2657  opabid 2863  uniuni 2935  elvvv 3287  dmuni 3383  dm0rn0 3390  dmcoss 3423  dmcosseq 3425  rnuni 3515  rnco 3575  coass 3586  imaiun 3940  iinon 3986  dfoprab2 4067  domen 4466  xpcomen 4526  xpassen 4528  scott0 4803  aceq5lem1 4821  aceq5lem4 4824  cflem 4994  genpass 5201  addcompr 5212  mulcompr 5214  ltexprlem1 5231  ltexprlem4 5234  reclem1pr 5245  reclem2pr 5246  suplem1pr 5250  rcfpfillem3 10718

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-4 1005  ax-5o 1007  ax-6o 1010

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1013

Copyright terms: Public domain