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

Theorem eeanv 1807
 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 1421 . 2 𝑦𝜑
2 nfv 1421 . 2 𝑥𝜓
31, 2eean 1806 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ 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-17 1419  ax-ial 1427 This theorem depends on definitions:  df-bi 110  df-nf 1350 This theorem is referenced by:  eeeanv  1808  ee4anv  1809  2eu4  1993  cgsex2g  2590  cgsex4g  2591  vtocl2  2609  spc2egv  2642  spc2gv  2643  dtruarb  3942  copsex2t  3982  copsex2g  3983  opelopabsb  3997  xpmlem  4744  fununi  4967  imain  4981  brabvv  5551  tfrlem7  5933  ener  6259  domtr  6265  unen  6293  ltexprlemdisj  6704  recexprlemdisj  6728
 Copyright terms: Public domain W3C validator