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

Theorem eeanv 1856
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 1467 . 2 𝑦𝜑
2 nfv 1467 . 2 𝑥𝜓
31, 2eean 1855 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104  wex 1427
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473
This theorem depends on definitions:  df-bi 116  df-nf 1396
This theorem is referenced by:  eeeanv  1857  ee4anv  1858  2eu4  2042  cgsex2g  2658  cgsex4g  2659  vtocl2  2677  spc2egv  2711  spc2gv  2712  dtruarb  4034  copsex2t  4083  copsex2g  4084  opelopabsb  4098  xpmlem  4867  fununi  5097  imain  5111  brabvv  5711  spc2ed  6014  tfrlem7  6098  ener  6552  domtr  6558  unen  6589  mapen  6618  sbthlemi10  6731  ltexprlemdisj  7228  recexprlemdisj  7252  hashfacen  10304  isummo  10836
  Copyright terms: Public domain W3C validator