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

Theorem r2ex 2872
Description: Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.)
Assertion
Ref Expression
r2ex  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. x E. y ( ( x  e.  A  /\  y  e.  B )  /\  ph ) )
Distinct variable groups:    x, y    y, A
Allowed substitution hints:    ph( x, y)    A( x)    B( x, y)

Proof of Theorem r2ex
StepHypRef Expression
1 nfcv 2614 . 2  |-  F/_ y A
21r2exf 2870 1  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. x E. y ( ( x  e.  A  /\  y  e.  B )  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1587    e. wcel 1758   E.wrex 2797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1588  df-nf 1591  df-sb 1703  df-cleq 2444  df-clel 2447  df-nfc 2602  df-rex 2802
This theorem is referenced by:  reean  2987  rnoprab2  6279  elrnmpt2res  6309  oeeu  7147  omxpenlem  7517  axcnre  9437  pmtrrn2  16080  fsumvma  22680  usgrarnedg  23450  spanuni  25094  5oalem7  25210  3oalem3  25214  elfuns  28085  ellines  28322  hash2prv  30369  hash2sspr  30370  dalem20  33656  diblsmopel  35135
  Copyright terms: Public domain W3C validator