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

Theorem rexlimivv 2672
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)
Hypothesis
Ref Expression
rexlimivv.1  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
rexlimivv  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Distinct variable groups:    x, y, ps    y, A
Allowed substitution hints:    ph( x, y)    A( x)    B( x, y)

Proof of Theorem rexlimivv
StepHypRef Expression
1 rexlimivv.1 . . 3  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ( ph  ->  ps ) )
21rexlimdva 2667 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2661 1  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  2reu5  2973  opelxp  4719  opiota  6290  tfrlem5  6396  xpdom2  6957  1sdom  7065  unxpdomlem3  7069  unfi  7124  elfiun  7183  xpnum  7584  kmlem9  7784  nqereu  8553  distrlem5pr  8651  mulid1  8835  1re  8837  mul02  8990  cnegex  8993  recex  9400  creur  9740  creui  9741  cju  9742  elz2  10040  zaddcl  10059  qre  10321  qaddcl  10332  qnegcl  10333  qmulcl  10334  qreccl  10336  replim  11601  xpnnenOLD  12488  odd2np1  12587  qredeu  12786  opoe  12864  omoe  12865  opeo  12866  omeo  12867  pythagtriplem1  12869  pcz  12933  4sqlem1  12995  4sqlem2  12996  4sqlem4  12999  mul4sq  13001  efgmnvl  15023  efgrelexlema  15058  txuni2  17260  tx2ndc  17345  blssioo  18301  tgioo  18302  ioorf  18928  ioorinv  18931  ioorcl  18932  dyaddisj  18951  mbfid  18991  elply  19577  vmacl  20356  efvmacl  20358  vmalelog  20444  2sqlem2  20603  mul2sq  20604  2sqlem7  20609  pntibnd  20742  ostth  20788  lpni  20846  ipasslem5  21413  ipasslem11  21418  hhssnv  21841  shscli  21896  shsleji  21949  shsidmi  21963  spansncvi  22231  superpos  22934  chirredi  22974  mdsymlem6  22988  rnmpt2ss  23239  cnre2csqima  23295  ghomgrpilem2  23993  poseq  24253  soseq  24254  nofulllem5  24360  elaltxp  24509  altxpsspw  24511  funtransport  24654  funray  24763  funline  24765  ellines  24775  linethru  24776  limptlimpr2lem2  25575  intvconlem1  25703  gltpntl  26072  mzpcompact2lem  26829  2reu4  27968  isline  29928
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator