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

Theorem excom 1664
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
excom (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)

Proof of Theorem excom
StepHypRef Expression
1 excomim 1663 . 2 (∃𝑥𝑦𝜑 → ∃𝑦𝑥𝜑)
2 excomim 1663 . 2 (∃𝑦𝑥𝜑 → ∃𝑥𝑦𝜑)
31, 2impbii 126 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wb 105  wex 1492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  excom13  1689  exrot3  1690  ee4anv  1934  sbexyz  2003  2exsb  2009  2euex  2113  2exeu  2118  2eu4  2119  rexcomf  2639  gencbvex  2783  euxfr2dc  2922  euind  2924  sbccomlem  3037  opelopabsbALT  4259  uniuni  4451  elvvv  4689  elco  4793  dmuni  4837  dm0rn0  4844  dmmrnm  4846  dmcosseq  4898  elres  4943  rnco  5135  coass  5147  oprabid  5906  dfoprab2  5921  opabex3d  6121  opabex3  6122  cnvoprab  6234  domen  6750  xpassen  6829  prarloc  7501  fisumcom2  11441  fprodcom2fi  11629
  Copyright terms: Public domain W3C validator