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

Theorem eeanv 1823
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 1437 . 2 𝑦𝜑
2 nfv 1437 . 2 𝑥𝜓
31, 2eean 1822 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Colors of variables: wff set class
Syntax hints:  wa 101  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-17 1435  ax-ial 1443
This theorem depends on definitions:  df-bi 114  df-nf 1366
This theorem is referenced by:  eeeanv  1824  ee4anv  1825  2eu4  2009  cgsex2g  2607  cgsex4g  2608  vtocl2  2626  spc2egv  2659  spc2gv  2660  dtruarb  3970  copsex2t  4010  copsex2g  4011  opelopabsb  4025  xpmlem  4772  fununi  4995  imain  5009  brabvv  5579  spc2ed  5882  tfrlem7  5964  ener  6290  domtr  6296  unen  6324  ltexprlemdisj  6762  recexprlemdisj  6786
  Copyright terms: Public domain W3C validator