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

Theorem r2ex 3195
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 3194 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → ¬ 𝜑))
21r2exlem 3143 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 396  wex 1781  wcel 2106  wrex 3070
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 3062  df-rex 3071
This theorem is referenced by:  reeanlem  3225  elxp2  5699  elinxp  6017  rnoprab2  7509  elrnmpores  7542  oeeu  8599  omxpenlem  9069  axcnre  11155  hash2prb  14429  hashle2prv  14435  pmtrrn2  19322  fsumvma  26705  umgredg  28387  fusgr2wsp2nb  29576  spanuni  30784  5oalem7  30900  3oalem3  30904  trsp2cyc  32269  fmla0xp  34362  elfuns  34875  ellines  35112  dalem20  38552  diblsmopel  40030  iunrelexpuztr  42455  sprssspr  46135  prprelb  46170
  Copyright terms: Public domain W3C validator