MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r2ex Structured version   Visualization version   GIF version

Theorem r2ex 3209
Description: Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020.)
Assertion
Ref Expression
r2ex (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem r2ex
StepHypRef Expression
1 r2al 3088 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → ¬ 𝜑))
21r2exlem 3207 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 382  wex 1852  wcel 2145  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-ral 3066  df-rex 3067
This theorem is referenced by:  reean  3254  elxp2  5273  rnoprab2  6895  elrnmpt2res  6925  oeeu  7841  omxpenlem  8221  axcnre  10191  hash2prb  13456  hashle2prv  13462  pmtrrn2  18087  fsumvma  25159  umgredg  26255  fusgr2wsp2nb  27516  spanuni  28743  5oalem7  28859  3oalem3  28863  elfuns  32359  ellines  32596  cnfinltrel  33578  dalem20  35502  diblsmopel  36981  iunrelexpuztr  38537  sprssspr  42256
  Copyright terms: Public domain W3C validator