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

Theorem rexlimivv 2951
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 2946 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2940 1  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    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:  2reu5  3305  opelxp  5018  opiota  6832  f1o2ndf1  6881  tfrlem5  7041  xpdom2  7605  1sdom  7715  unxpdomlem3  7719  unfi  7779  elfiun  7882  xpnum  8323  kmlem9  8529  nqereu  9296  distrlem5pr  9394  mulid1  9582  1re  9584  mul02  9747  cnegex  9750  recex  10177  creur  10525  creui  10526  cju  10527  elz2  10877  zaddcl  10900  qre  11188  qaddcl  11199  qnegcl  11200  qmulcl  11201  qreccl  11203  replim  13031  prodmo  13825  xpnnenOLD  14027  odd2np1  14130  qredeu  14332  opoe  14419  omoe  14420  opeo  14421  omeo  14422  pythagtriplem1  14424  pcz  14488  4sqlem1  14550  4sqlem2  14551  4sqlem4  14554  mul4sq  14556  pmtr3ncom  16699  efgmnvl  16931  efgrelexlema  16966  ring1ne0  17434  txuni2  20232  tx2ndc  20318  blssioo  21466  tgioo  21467  ioorf  22148  ioorinv  22151  ioorcl  22152  dyaddisj  22171  mbfid  22209  elply  22758  vmacl  23590  efvmacl  23592  vmalelog  23678  2sqlem2  23837  mul2sq  23838  2sqlem7  23843  pntibnd  23976  ostth  24022  legval  24172  usgrasscusgra  24685  el2wlksoton  25080  el2spthsoton  25081  n4cyclfrgra  25220  vdn0frgrav2  25225  vdgn0frgrav2  25226  vdn1frgrav2  25227  vdgn1frgrav2  25228  2spotmdisj  25270  friendshipgt3  25323  lpni  25383  ipasslem5  25948  ipasslem11  25953  hhssnv  26378  shscli  26433  shsleji  26486  shsidmi  26500  spansncvi  26768  superpos  27471  chirredi  27511  mdsymlem6  27525  rnmpt2ss  27742  cnre2csqima  28128  dya2icobrsiga  28484  dya2iocnrect  28489  dya2iocucvr  28492  sxbrsigalem2  28494  afsval  28815  msubco  29155  ghomgrpilem2  29290  poseq  29573  soseq  29574  nofulllem5  29706  elaltxp  29853  altxpsspw  29855  funtransport  29909  funray  30018  funline  30020  ellines  30030  linethru  30031  itg2addnc  30309  mzpcompact2lem  30923  2reu4  32434  usgvincvad  32776  usgvincvadALT  32779  nnpw2pb  33462  isline  35860
  Copyright terms: Public domain W3C validator