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

Theorem r2ex 3189
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 3188 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → ¬ 𝜑))
21r2exlem 3137 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 397  wex 1782  wcel 2107  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3062  df-rex 3071
This theorem is referenced by:  reeanlem  3215  elxp2  5658  elinxp  5976  rnoprab2  7462  elrnmpores  7494  oeeu  8551  omxpenlem  9020  axcnre  11105  hash2prb  14377  hashle2prv  14383  pmtrrn2  19247  fsumvma  26577  umgredg  28131  fusgr2wsp2nb  29320  spanuni  30528  5oalem7  30644  3oalem3  30648  trsp2cyc  32021  fmla0xp  34034  elfuns  34546  ellines  34783  dalem20  38202  diblsmopel  39680  iunrelexpuztr  42079  sprssspr  45759  prprelb  45794
  Copyright terms: Public domain W3C validator