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

Theorem r2ex 3222
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 3122 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → ¬ 𝜑))
21r2exlem 3221 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wa 399  wex 1787  wcel 2110  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3066  df-rex 3067
This theorem is referenced by:  reeanlem  3277  elxp2  5575  elinxp  5889  rnoprab2  7315  elrnmpores  7347  oeeu  8331  omxpenlem  8746  axcnre  10778  hash2prb  14038  hashle2prv  14044  pmtrrn2  18852  fsumvma  26094  umgredg  27229  fusgr2wsp2nb  28417  spanuni  29625  5oalem7  29741  3oalem3  29745  trsp2cyc  31109  fmla0xp  33058  elfuns  33954  ellines  34191  dalem20  37444  diblsmopel  38922  iunrelexpuztr  41004  sprssspr  44606  prprelb  44641
  Copyright terms: Public domain W3C validator