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

Theorem r2ex 3192
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 3191 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → ¬ 𝜑))
21r2exlem 3140 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 396  wex 1781  wcel 2106  wrex 3073
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 1913
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3065  df-rex 3074
This theorem is referenced by:  reeanlem  3216  elxp2  5657  elinxp  5975  rnoprab2  7460  elrnmpores  7492  oeeu  8549  omxpenlem  9016  axcnre  11099  hash2prb  14370  hashle2prv  14376  pmtrrn2  19240  fsumvma  26559  umgredg  28036  fusgr2wsp2nb  29225  spanuni  30433  5oalem7  30549  3oalem3  30553  trsp2cyc  31916  fmla0xp  33917  elfuns  34490  ellines  34727  dalem20  38146  diblsmopel  39624  iunrelexpuztr  41972  sprssspr  45644  prprelb  45679
  Copyright terms: Public domain W3C validator