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