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

Theorem r2ex 3186
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 3185 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → ¬ 𝜑))
21r2exlem 3133 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 394  wex 1774  wcel 2099  wrex 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-ral 3052  df-rex 3061
This theorem is referenced by:  reeanlem  3216  elxp2  5706  elinxp  6028  rnoprab2  7530  elrnmpores  7564  oeeu  8633  omxpenlem  9111  axcnre  11207  hash2prb  14491  hashle2prv  14497  pmtrrn2  19458  fsumvma  27242  umgredg  29074  fusgr2wsp2nb  30267  spanuni  31477  5oalem7  31593  3oalem3  31597  trsp2cyc  33001  fmla0xp  35211  elfuns  35739  ellines  35976  dalem20  39392  diblsmopel  40870  iunrelexpuztr  43386  sprssspr  47053  prprelb  47088
  Copyright terms: Public domain W3C validator