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

Theorem rexlimivv 2836
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 2831 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2825 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 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711
This theorem is referenced by:  2reu5  3156  opelxp  4856  opiota  6622  f1o2ndf1  6669  xpdom2  7394  1sdom  7503  unxpdomlem3  7507  unfi  7567  elfiun  7668  xpnum  8109  kmlem9  8315  nqereu  9085  distrlem5pr  9183  mulid1  9370  1re  9372  mul02  9534  cnegex  9537  recex  9955  creur  10303  creui  10304  cju  10305  elz2  10650  zaddcl  10672  qre  10945  qaddcl  10956  qnegcl  10957  qmulcl  10958  qreccl  10960  replim  12588  xpnnenOLD  13474  odd2np1  13574  qredeu  13775  opoe  13860  omoe  13861  opeo  13862  omeo  13863  pythagtriplem1  13865  pcz  13929  4sqlem1  13991  4sqlem2  13992  4sqlem4  13995  mul4sq  13997  pmtr3ncom  15960  efgmnvl  16190  efgrelexlema  16225  txuni2  18979  tx2ndc  19065  blssioo  20213  tgioo  20214  ioorf  20894  ioorinv  20897  ioorcl  20898  dyaddisj  20917  mbfid  20955  elply  21547  vmacl  22340  efvmacl  22342  vmalelog  22428  2sqlem2  22587  mul2sq  22588  2sqlem7  22593  pntibnd  22726  ostth  22772  legval  22890  usgrasscusgra  23213  lpni  23488  ipasslem5  24057  ipasslem11  24062  hhssnv  24487  shscli  24542  shsleji  24595  shsidmi  24609  spansncvi  24877  superpos  25580  chirredi  25620  mdsymlem6  25634  rnmpt2ss  25815  cnre2csqima  26194  dya2icobrsiga  26544  dya2iocnrect  26549  dya2iocucvr  26552  sxbrsigalem2  26554  ghomgrpilem2  27151  prodmo  27295  poseq  27560  soseq  27561  nofulllem5  27693  elaltxp  27852  altxpsspw  27854  funtransport  27908  funray  28017  funline  28019  ellines  28029  linethru  28030  itg2addnc  28287  mzpcompact2lem  28930  2reu4  29857  el2wlksoton  30240  el2spthsoton  30241  n4cyclfrgra  30453  vdn0frgrav2  30459  vdgn0frgrav2  30460  vdn1frgrav2  30461  vdgn1frgrav2  30462  2spotmdisj  30504  friendshipgt3  30557  rng1ne0  30601  isline  32953
  Copyright terms: Public domain W3C validator