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

Theorem r2ex 3266
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 3168 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → ¬ 𝜑))
21r2exlem 3265 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wa 396  wex 1761  wcel 2081  wrex 3106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-ral 3110  df-rex 3111
This theorem is referenced by:  rexcomOLD  3317  reeanlem  3326  elxp2  5472  elinxp  5776  rnoprab2  7119  elrnmpores  7149  oeeu  8084  omxpenlem  8470  axcnre  10437  hash2prb  13681  hashle2prv  13687  pmtrrn2  18324  fsumvma  25476  umgredg  26611  fusgr2wsp2nb  27810  spanuni  29017  5oalem7  29133  3oalem3  29137  trsp2cyc  30417  fmla0xp  32244  elfuns  32991  ellines  33228  dalem20  36385  diblsmopel  37863  iunrelexpuztr  39574  sprssspr  43151  prprelb  43186
  Copyright terms: Public domain W3C validator