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

Theorem r2ex 3194
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 3193 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → ¬ 𝜑))
21r2exlem 3141 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395  wex 1776  wcel 2106  wrex 3068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060  df-rex 3069
This theorem is referenced by:  r3ex  3196  reeanlem  3226  elxp2  5713  elinxp  6039  rnoprab2  7538  elrnmpores  7571  oeeu  8640  omxpenlem  9112  axcnre  11202  hash2prb  14508  hashle2prv  14514  pmtrrn2  19493  fsumvma  27272  umgredg  29170  fusgr2wsp2nb  30363  spanuni  31573  5oalem7  31689  3oalem3  31693  trsp2cyc  33126  fmla0xp  35368  elfuns  35897  ellines  36134  dalem20  39676  diblsmopel  41154  iunrelexpuztr  43709  sprssspr  47406  prprelb  47441
  Copyright terms: Public domain W3C validator