ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  excom Unicode version

Theorem excom 1599
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
StepHypRef Expression
1 excomim 1598 . 2  |-  ( E. x E. y ph  ->  E. y E. x ph )
2 excomim 1598 . 2  |-  ( E. y E. x ph  ->  E. x E. y ph )
31, 2impbii 124 1  |-  ( E. x E. y ph  <->  E. y E. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   E.wex 1426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-ial 1472
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  excom13  1624  exrot3  1625  ee4anv  1857  sbexyz  1927  2exsb  1933  2euex  2035  2exeu  2040  2eu4  2041  rexcomf  2529  gencbvex  2665  euxfr2dc  2800  euind  2802  sbccomlem  2913  opelopabsbALT  4084  uniuni  4271  elvvv  4497  elco  4598  dmuni  4642  dm0rn0  4649  dmmrnm  4651  dmcosseq  4700  elres  4743  rnco  4932  coass  4944  oprabid  5673  dfoprab2  5688  opabex3d  5884  opabex3  5885  cnvoprab  5991  domen  6458  xpassen  6536  prarloc  7052  fisumcom2  10819
  Copyright terms: Public domain W3C validator