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

Theorem rexlimivv 2960
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 2955 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2949 1  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  2reu5  3312  opelxp  5029  opiota  6843  f1o2ndf1  6891  xpdom2  7612  1sdom  7722  unxpdomlem3  7726  unfi  7787  elfiun  7890  xpnum  8332  kmlem9  8538  nqereu  9307  distrlem5pr  9405  mulid1  9593  1re  9595  mul02  9757  cnegex  9760  recex  10181  creur  10530  creui  10531  cju  10532  elz2  10881  zaddcl  10903  qre  11187  qaddcl  11198  qnegcl  11199  qmulcl  11200  qreccl  11202  replim  12912  xpnnenOLD  13804  odd2np1  13905  qredeu  14107  opoe  14194  omoe  14195  opeo  14196  omeo  14197  pythagtriplem1  14199  pcz  14263  4sqlem1  14325  4sqlem2  14326  4sqlem4  14329  mul4sq  14331  pmtr3ncom  16306  efgmnvl  16538  efgrelexlema  16573  rng1ne0  17040  txuni2  19829  tx2ndc  19915  blssioo  21063  tgioo  21064  ioorf  21745  ioorinv  21748  ioorcl  21749  dyaddisj  21768  mbfid  21806  elply  22355  vmacl  23148  efvmacl  23150  vmalelog  23236  2sqlem2  23395  mul2sq  23396  2sqlem7  23401  pntibnd  23534  ostth  23580  legval  23726  usgrasscusgra  24187  el2wlksoton  24582  el2spthsoton  24583  n4cyclfrgra  24722  vdn0frgrav2  24728  vdgn0frgrav2  24729  vdn1frgrav2  24730  vdgn1frgrav2  24731  2spotmdisj  24773  friendshipgt3  24826  lpni  24885  ipasslem5  25454  ipasslem11  25459  hhssnv  25884  shscli  25939  shsleji  25992  shsidmi  26006  spansncvi  26274  superpos  26977  chirredi  27017  mdsymlem6  27031  rnmpt2ss  27215  cnre2csqima  27557  dya2icobrsiga  27915  dya2iocnrect  27920  dya2iocucvr  27923  sxbrsigalem2  27925  ghomgrpilem2  28529  prodmo  28673  poseq  28938  soseq  28939  nofulllem5  29071  elaltxp  29230  altxpsspw  29232  funtransport  29286  funray  29395  funline  29397  ellines  29407  linethru  29408  itg2addnc  29674  mzpcompact2lem  30316  2reu4  31690  usgvincvad  31899  usgvincvadALT  31902  isline  34553
  Copyright terms: Public domain W3C validator