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

Theorem excom 1595
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 1594 . 2  |-  ( E. x E. y ph  ->  E. y E. x ph )
2 excomim 1594 . 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 1422
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-ial 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  excom13  1620  exrot3  1621  ee4anv  1851  sbexyz  1921  2exsb  1927  2euex  2029  2exeu  2034  2eu4  2035  rexcomf  2517  gencbvex  2646  euxfr2dc  2778  euind  2780  sbccomlem  2889  opelopabsbALT  4022  uniuni  4209  elvvv  4429  dmuni  4573  dm0rn0  4580  dmmrnm  4582  dmcosseq  4631  elres  4674  rnco  4857  coass  4869  oprabid  5568  dfoprab2  5583  opabex3d  5779  opabex3  5780  cnvoprab  5886  domen  6298  xpassen  6374  prarloc  6755
  Copyright terms: Public domain W3C validator