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

Theorem excom 1554
 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 1553 . 2 (∃𝑥𝑦𝜑 → ∃𝑦𝑥𝜑)
2 excomim 1553 . 2 (∃𝑦𝑥𝜑 → ∃𝑥𝑦𝜑)
31, 2impbii 117 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98  ∃wex 1381 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-ial 1427 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  excom13  1579  exrot3  1580  ee4anv  1809  sbexyz  1879  2exsb  1885  2euex  1987  2exeu  1992  2eu4  1993  rexcomf  2472  gencbvex  2600  euxfr2dc  2726  euind  2728  sbccomlem  2832  opelopabsbALT  3996  uniuni  4183  elvvv  4403  dmuni  4545  dm0rn0  4552  dmmrnm  4554  dmcosseq  4603  elres  4646  rnco  4827  coass  4839  oprabid  5537  dfoprab2  5552  opabex3d  5748  opabex3  5749  domen  6232  xpassen  6304  prarloc  6601
 Copyright terms: Public domain W3C validator