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

Theorem excom 1597
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 1596 . 2 (∃𝑥𝑦𝜑 → ∃𝑦𝑥𝜑)
2 excomim 1596 . 2 (∃𝑦𝑥𝜑 → ∃𝑥𝑦𝜑)
31, 2impbii 124 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wb 103  wex 1424
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-ial 1470
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  excom13  1622  exrot3  1623  ee4anv  1854  sbexyz  1924  2exsb  1930  2euex  2032  2exeu  2037  2eu4  2038  rexcomf  2525  gencbvex  2659  euxfr2dc  2791  euind  2793  sbccomlem  2902  opelopabsbALT  4060  uniuni  4247  elvvv  4469  elco  4570  dmuni  4614  dm0rn0  4621  dmmrnm  4623  dmcosseq  4672  elres  4715  rnco  4903  coass  4915  oprabid  5638  dfoprab2  5653  opabex3d  5849  opabex3  5850  cnvoprab  5956  domen  6420  xpassen  6498  prarloc  7006
  Copyright terms: Public domain W3C validator