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

Theorem eeanv 1904
 Description: Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
Assertion
Ref Expression
eeanv (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Distinct variable groups:   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem eeanv
StepHypRef Expression
1 nfv 1508 . 2 𝑦𝜑
2 nfv 1508 . 2 𝑥𝜓
31, 2eean 1903 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104  ∃wex 1468 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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514 This theorem depends on definitions:  df-bi 116  df-nf 1437 This theorem is referenced by:  eeeanv  1905  ee4anv  1906  2eu4  2092  cgsex2g  2722  cgsex4g  2723  vtocl2  2741  spc2egv  2775  spc2gv  2776  dtruarb  4115  copsex2t  4167  copsex2g  4168  opelopabsb  4182  xpmlem  4959  fununi  5191  imain  5205  brabvv  5817  spc2ed  6130  tfrlem7  6214  ener  6673  domtr  6679  unen  6710  mapen  6740  sbthlemi10  6854  ltexprlemdisj  7421  recexprlemdisj  7445  hashfacen  10586  summodc  11159
 Copyright terms: Public domain W3C validator