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

Theorem r2ex 2980
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:   ,   ,

Proof of Theorem r2ex
StepHypRef Expression
1 r2al 2835 . 2
21r2exlem 2977 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  /\wa 369  E.wex 1612  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  reean  3024  rnoprab2  6386  elrnmpt2res  6416  oeeu  7271  omxpenlem  7638  axcnre  9562  hash2prv  12525  hash2sspr  12526  pmtrrn2  16485  fsumvma  23488  usgrarnedg  24384  spanuni  26462  5oalem7  26578  3oalem3  26582  elfuns  29565  ellines  29802  usgedgimp  32403  usgedgimpALT  32406  dalem20  35417  diblsmopel  36898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813
  Copyright terms: Public domain W3C validator