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

Theorem excom 1595
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 1594 . 2 (∃𝑥𝑦𝜑 → ∃𝑦𝑥𝜑)
2 excomim 1594 . 2 (∃𝑦𝑥𝜑 → ∃𝑥𝑦𝜑)
31, 2impbii 124 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wb 103  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  1852  sbexyz  1922  2exsb  1928  2euex  2030  2exeu  2035  2eu4  2036  rexcomf  2522  gencbvex  2656  euxfr2dc  2788  euind  2790  sbccomlem  2899  opelopabsbALT  4050  uniuni  4237  elvvv  4459  elco  4560  dmuni  4604  dm0rn0  4611  dmmrnm  4613  dmcosseq  4662  elres  4705  rnco  4891  coass  4903  oprabid  5616  dfoprab2  5631  opabex3d  5827  opabex3  5828  cnvoprab  5934  domen  6398  xpassen  6476  prarloc  6965
  Copyright terms: Public domain W3C validator