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

Theorem r2ex 2977
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  |-  ( 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 r2al 2832 . 2  |-  ( A. x  e.  A  A. y  e.  B  -.  ph  <->  A. x A. y ( ( x  e.  A  /\  y  e.  B
)  ->  -.  ph )
)
21r2exlem 2974 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:   -. wn 3    <-> wb 184    /\ wa 367   E.wex 1617    e. wcel 1823   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-ral 2809  df-rex 2810
This theorem is referenced by:  reean  3021  rnoprab2  6359  elrnmpt2res  6389  oeeu  7244  omxpenlem  7611  axcnre  9530  hash2prv  12509  hash2sspr  12510  pmtrrn2  16684  fsumvma  23686  usgrarnedg  24586  spanuni  26660  5oalem7  26776  3oalem3  26780  elfuns  29793  ellines  30030  usgedgimp  32775  usgedgimpALT  32778  dalem20  35814  diblsmopel  37295  iunrelexpuztr  38206
  Copyright terms: Public domain W3C validator