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

Theorem rexlimivv 2837
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 2832 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2826 1  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726   E.wrex 2708
This theorem is referenced by:  2reu5  3144  opelxp  4911  f1o2ndf1  6457  opiota  6538  tfrlem5  6644  xpdom2  7206  1sdom  7314  unxpdomlem3  7318  unfi  7377  elfiun  7438  xpnum  7843  kmlem9  8043  nqereu  8811  distrlem5pr  8909  mulid1  9093  1re  9095  mul02  9249  cnegex  9252  recex  9659  creur  9999  creui  10000  cju  10001  elz2  10303  zaddcl  10322  qre  10584  qaddcl  10595  qnegcl  10596  qmulcl  10597  qreccl  10599  replim  11926  xpnnenOLD  12814  odd2np1  12913  qredeu  13112  opoe  13190  omoe  13191  opeo  13192  omeo  13193  pythagtriplem1  13195  pcz  13259  4sqlem1  13321  4sqlem2  13322  4sqlem4  13325  mul4sq  13327  efgmnvl  15351  efgrelexlema  15386  txuni2  17602  tx2ndc  17688  blssioo  18831  tgioo  18832  ioorf  19470  ioorinv  19473  ioorcl  19474  dyaddisj  19493  mbfid  19531  elply  20119  vmacl  20906  efvmacl  20908  vmalelog  20994  2sqlem2  21153  mul2sq  21154  2sqlem7  21159  pntibnd  21292  ostth  21338  usgrasscusgra  21497  lpni  21772  ipasslem5  22341  ipasslem11  22346  hhssnv  22769  shscli  22824  shsleji  22877  shsidmi  22891  spansncvi  23159  superpos  23862  chirredi  23902  mdsymlem6  23916  rnmpt2ss  24091  cnre2csqima  24314  dya2icobrsiga  24631  dya2iocnrect  24636  dya2iocucvr  24639  sxbrsigalem2  24641  ghomgrpilem2  25102  prodmo  25267  poseq  25533  soseq  25534  nofulllem5  25666  elaltxp  25825  altxpsspw  25827  funtransport  25970  funray  26079  funline  26081  ellines  26091  linethru  26092  itg2addnc  26273  mzpcompact2lem  26822  2reu4  27958  el2wlksoton  28410  el2spthsoton  28411  n4cyclfrgra  28482  vdn0frgrav2  28488  vdgn0frgrav2  28489  vdn1frgrav2  28490  vdgn1frgrav2  28491  2spotmdisj  28531  isline  30610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2712  df-rex 2713
  Copyright terms: Public domain W3C validator