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

Theorem r2ex 3262
 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 3166 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → ¬ 𝜑))
21r2exlem 3261 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112 This theorem is referenced by:  rexcomOLD  3309  reeanlem  3318  elxp2  5543  elinxp  5856  rnoprab2  7237  elrnmpores  7268  oeeu  8214  omxpenlem  8603  axcnre  10577  hash2prb  13828  hashle2prv  13834  pmtrrn2  18583  fsumvma  25804  umgredg  26938  fusgr2wsp2nb  28126  spanuni  29334  5oalem7  29450  3oalem3  29454  trsp2cyc  30822  fmla0xp  32755  elfuns  33501  ellines  33738  dalem20  37005  diblsmopel  38483  iunrelexpuztr  40435  sprssspr  44013  prprelb  44048
 Copyright terms: Public domain W3C validator