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

Theorem excom 1570
 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 1569 . 2 (∃𝑥𝑦𝜑 → ∃𝑦𝑥𝜑)
2 excomim 1569 . 2 (∃𝑦𝑥𝜑 → ∃𝑥𝑦𝜑)
31, 2impbii 121 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
 Colors of variables: wff set class Syntax hints:   ↔ wb 102  ∃wex 1397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-ial 1443 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  excom13  1595  exrot3  1596  ee4anv  1825  sbexyz  1895  2exsb  1901  2euex  2003  2exeu  2008  2eu4  2009  rexcomf  2489  gencbvex  2617  euxfr2dc  2748  euind  2750  sbccomlem  2859  opelopabsbALT  4023  uniuni  4210  elvvv  4430  dmuni  4572  dm0rn0  4579  dmmrnm  4581  dmcosseq  4630  elres  4673  rnco  4854  coass  4866  oprabid  5564  dfoprab2  5579  opabex3d  5775  opabex3  5776  cnvoprab  5882  domen  6262  xpassen  6334  prarloc  6658
 Copyright terms: Public domain W3C validator