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

Theorem rexlimivv 2938
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 2933 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2927 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 1802   E.wrex 2792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-ral 2796  df-rex 2797
This theorem is referenced by:  2reu5  3292  opelxp  5015  opiota  6840  f1o2ndf1  6889  tfrlem5  7047  xpdom2  7610  1sdom  7720  unxpdomlem3  7724  unfi  7785  elfiun  7888  xpnum  8330  kmlem9  8536  nqereu  9305  distrlem5pr  9403  mulid1  9591  1re  9593  mul02  9756  cnegex  9759  recex  10182  creur  10531  creui  10532  cju  10533  elz2  10882  zaddcl  10905  qre  11191  qaddcl  11202  qnegcl  11203  qmulcl  11204  qreccl  11206  replim  12923  xpnnenOLD  13815  odd2np1  13918  qredeu  14120  opoe  14207  omoe  14208  opeo  14209  omeo  14210  pythagtriplem1  14212  pcz  14276  4sqlem1  14338  4sqlem2  14339  4sqlem4  14342  mul4sq  14344  pmtr3ncom  16369  efgmnvl  16601  efgrelexlema  16636  ring1ne0  17107  txuni2  19932  tx2ndc  20018  blssioo  21166  tgioo  21167  ioorf  21848  ioorinv  21851  ioorcl  21852  dyaddisj  21871  mbfid  21909  elply  22458  vmacl  23257  efvmacl  23259  vmalelog  23345  2sqlem2  23504  mul2sq  23505  2sqlem7  23510  pntibnd  23643  ostth  23689  legval  23836  usgrasscusgra  24348  el2wlksoton  24743  el2spthsoton  24744  n4cyclfrgra  24883  vdn0frgrav2  24888  vdgn0frgrav2  24889  vdn1frgrav2  24890  vdgn1frgrav2  24891  2spotmdisj  24933  friendshipgt3  24986  lpni  25046  ipasslem5  25615  ipasslem11  25620  hhssnv  26045  shscli  26100  shsleji  26153  shsidmi  26167  spansncvi  26435  superpos  27138  chirredi  27178  mdsymlem6  27192  rnmpt2ss  27380  cnre2csqima  27759  dya2icobrsiga  28113  dya2iocnrect  28118  dya2iocucvr  28121  sxbrsigalem2  28123  afsval  28417  msubco  28757  ghomgrpilem2  28892  prodmo  29036  poseq  29301  soseq  29302  nofulllem5  29434  elaltxp  29593  altxpsspw  29595  funtransport  29649  funray  29758  funline  29760  ellines  29770  linethru  29771  itg2addnc  30037  mzpcompact2lem  30652  2reu4  32029  usgvincvad  32238  usgvincvadALT  32241  isline  35165
  Copyright terms: Public domain W3C validator