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

Theorem excom 1625
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 1624 . 2 (∃𝑥𝑦𝜑 → ∃𝑦𝑥𝜑)
2 excomim 1624 . 2 (∃𝑦𝑥𝜑 → ∃𝑥𝑦𝜑)
31, 2impbii 125 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104  wex 1451
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  excom13  1650  exrot3  1651  ee4anv  1884  sbexyz  1954  2exsb  1960  2euex  2062  2exeu  2067  2eu4  2068  rexcomf  2568  gencbvex  2704  euxfr2dc  2840  euind  2842  sbccomlem  2953  opelopabsbALT  4149  uniuni  4340  elvvv  4570  elco  4673  dmuni  4717  dm0rn0  4724  dmmrnm  4726  dmcosseq  4778  elres  4823  rnco  5013  coass  5025  oprabid  5769  dfoprab2  5784  opabex3d  5985  opabex3  5986  cnvoprab  6097  domen  6611  xpassen  6690  prarloc  7275  fisumcom2  11147
  Copyright terms: Public domain W3C validator