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

Theorem excom 1627
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 1626 . 2  |-  ( E. x E. y ph  ->  E. y E. x ph )
2 excomim 1626 . 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 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-ial 1499
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  excom13  1652  exrot3  1653  ee4anv  1886  sbexyz  1956  2exsb  1962  2euex  2064  2exeu  2069  2eu4  2070  rexcomf  2570  gencbvex  2706  euxfr2dc  2842  euind  2844  sbccomlem  2955  opelopabsbALT  4151  uniuni  4342  elvvv  4572  elco  4675  dmuni  4719  dm0rn0  4726  dmmrnm  4728  dmcosseq  4780  elres  4825  rnco  5015  coass  5027  oprabid  5771  dfoprab2  5786  opabex3d  5987  opabex3  5988  cnvoprab  6099  domen  6613  xpassen  6692  prarloc  7279  fisumcom2  11175
  Copyright terms: Public domain W3C validator