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

Theorem rexlimivv 2867
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 2862 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2856 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 1756   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2741  df-rex 2742
This theorem is referenced by:  2reu5  3188  opelxp  4890  opiota  6654  f1o2ndf1  6701  xpdom2  7427  1sdom  7536  unxpdomlem3  7540  unfi  7600  elfiun  7701  xpnum  8142  kmlem9  8348  nqereu  9119  distrlem5pr  9217  mulid1  9404  1re  9406  mul02  9568  cnegex  9571  recex  9989  creur  10337  creui  10338  cju  10339  elz2  10684  zaddcl  10706  qre  10979  qaddcl  10990  qnegcl  10991  qmulcl  10992  qreccl  10994  replim  12626  xpnnenOLD  13513  odd2np1  13613  qredeu  13814  opoe  13899  omoe  13900  opeo  13901  omeo  13902  pythagtriplem1  13904  pcz  13968  4sqlem1  14030  4sqlem2  14031  4sqlem4  14034  mul4sq  14036  pmtr3ncom  16002  efgmnvl  16232  efgrelexlema  16267  txuni2  19160  tx2ndc  19246  blssioo  20394  tgioo  20395  ioorf  21075  ioorinv  21078  ioorcl  21079  dyaddisj  21098  mbfid  21136  elply  21685  vmacl  22478  efvmacl  22480  vmalelog  22566  2sqlem2  22725  mul2sq  22726  2sqlem7  22731  pntibnd  22864  ostth  22910  legval  23037  usgrasscusgra  23413  lpni  23688  ipasslem5  24257  ipasslem11  24262  hhssnv  24687  shscli  24742  shsleji  24795  shsidmi  24809  spansncvi  25077  superpos  25780  chirredi  25820  mdsymlem6  25834  rnmpt2ss  26014  cnre2csqima  26363  dya2icobrsiga  26713  dya2iocnrect  26718  dya2iocucvr  26721  sxbrsigalem2  26723  ghomgrpilem2  27327  prodmo  27471  poseq  27736  soseq  27737  nofulllem5  27869  elaltxp  28028  altxpsspw  28030  funtransport  28084  funray  28193  funline  28195  ellines  28205  linethru  28206  itg2addnc  28472  mzpcompact2lem  29114  2reu4  30040  el2wlksoton  30423  el2spthsoton  30424  n4cyclfrgra  30636  vdn0frgrav2  30642  vdgn0frgrav2  30643  vdn1frgrav2  30644  vdgn1frgrav2  30645  2spotmdisj  30687  friendshipgt3  30740  rng1ne0  30803  isline  33479
  Copyright terms: Public domain W3C validator