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

Theorem excom 1644
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 1643 . 2 (∃𝑥𝑦𝜑 → ∃𝑦𝑥𝜑)
2 excomim 1643 . 2 (∃𝑦𝑥𝜑 → ∃𝑥𝑦𝜑)
31, 2impbii 125 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104  wex 1472
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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-ial 1514
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  excom13  1669  exrot3  1670  ee4anv  1914  sbexyz  1983  2exsb  1989  2euex  2093  2exeu  2098  2eu4  2099  rexcomf  2619  gencbvex  2758  euxfr2dc  2897  euind  2899  sbccomlem  3011  opelopabsbALT  4219  uniuni  4411  elvvv  4649  elco  4752  dmuni  4796  dm0rn0  4803  dmmrnm  4805  dmcosseq  4857  elres  4902  rnco  5092  coass  5104  oprabid  5853  dfoprab2  5868  opabex3d  6069  opabex3  6070  cnvoprab  6181  domen  6696  xpassen  6775  prarloc  7423  fisumcom2  11335  fprodcom2fi  11523
  Copyright terms: Public domain W3C validator