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

Theorem excom 1623
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 1622 . 2  |-  ( E. x E. y ph  ->  E. y E. x ph )
2 excomim 1622 . 2  |-  ( E. y E. x ph  ->  E. x E. y ph )
31, 2impbii 125 1  |-  ( E. x E. y ph  <->  E. y E. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   E.wex 1449
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-ial 1495
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  excom13  1648  exrot3  1649  ee4anv  1882  sbexyz  1952  2exsb  1958  2euex  2060  2exeu  2065  2eu4  2066  rexcomf  2565  gencbvex  2701  euxfr2dc  2836  euind  2838  sbccomlem  2949  opelopabsbALT  4139  uniuni  4330  elvvv  4560  elco  4663  dmuni  4707  dm0rn0  4714  dmmrnm  4716  dmcosseq  4766  elres  4811  rnco  5001  coass  5013  oprabid  5755  dfoprab2  5770  opabex3d  5971  opabex3  5972  cnvoprab  6083  domen  6597  xpassen  6675  prarloc  7253  fisumcom2  11093
  Copyright terms: Public domain W3C validator