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

Theorem r2ex 3043
 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 2923 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → ¬ 𝜑))
21r2exlem 3041 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ 𝜑))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902 This theorem is referenced by:  reean  3085  elxp2  5056  rnoprab2  6642  elrnmpt2res  6672  oeeu  7570  omxpenlem  7946  axcnre  9864  hash2prb  13111  pmtrrn2  17703  fsumvma  24738  upgredg  25811  umgredg  25812  usgrarnedg  25913  spanuni  27787  5oalem7  27903  3oalem3  27907  elfuns  31192  ellines  31429  dalem20  33997  diblsmopel  35478  iunrelexpuztr  37030
 Copyright terms: Public domain W3C validator