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

Theorem r2ex 3059
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 2938 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → ¬ 𝜑))
21r2exlem 3057 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 384  wex 1703  wcel 1989  wrex 2912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-ral 2916  df-rex 2917
This theorem is referenced by:  reean  3104  elxp2  5130  rnoprab2  6741  elrnmpt2res  6771  oeeu  7680  omxpenlem  8058  axcnre  9982  hash2prb  13249  hashle2prv  13255  pmtrrn2  17874  fsumvma  24932  umgredg  26027  fusgr2wsp2nb  27185  spanuni  28387  5oalem7  28503  3oalem3  28507  elfuns  32006  ellines  32243  dalem20  34805  diblsmopel  36286  iunrelexpuztr  37837  sprssspr  41502
  Copyright terms: Public domain W3C validator