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

Theorem rexlimivv 2827
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 2822 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2816 1  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  2reu5  3134  opelxp  4900  f1o2ndf1  6446  opiota  6527  tfrlem5  6633  xpdom2  7195  1sdom  7303  unxpdomlem3  7307  unfi  7366  elfiun  7427  xpnum  7830  kmlem9  8030  nqereu  8798  distrlem5pr  8896  mulid1  9080  1re  9082  mul02  9236  cnegex  9239  recex  9646  creur  9986  creui  9987  cju  9988  elz2  10290  zaddcl  10309  qre  10571  qaddcl  10582  qnegcl  10583  qmulcl  10584  qreccl  10586  replim  11913  xpnnenOLD  12801  odd2np1  12900  qredeu  13099  opoe  13177  omoe  13178  opeo  13179  omeo  13180  pythagtriplem1  13182  pcz  13246  4sqlem1  13308  4sqlem2  13309  4sqlem4  13312  mul4sq  13314  efgmnvl  15338  efgrelexlema  15373  txuni2  17589  tx2ndc  17675  blssioo  18818  tgioo  18819  ioorf  19457  ioorinv  19460  ioorcl  19461  dyaddisj  19480  mbfid  19520  elply  20106  vmacl  20893  efvmacl  20895  vmalelog  20981  2sqlem2  21140  mul2sq  21141  2sqlem7  21146  pntibnd  21279  ostth  21325  usgrasscusgra  21484  lpni  21759  ipasslem5  22328  ipasslem11  22333  hhssnv  22756  shscli  22811  shsleji  22864  shsidmi  22878  spansncvi  23146  superpos  23849  chirredi  23889  mdsymlem6  23903  rnmpt2ss  24078  cnre2csqima  24301  dya2icobrsiga  24618  dya2iocnrect  24623  dya2iocucvr  24626  sxbrsigalem2  24628  ghomgrpilem2  25089  prodmo  25254  poseq  25520  soseq  25521  nofulllem5  25653  elaltxp  25812  altxpsspw  25814  funtransport  25957  funray  26066  funline  26068  ellines  26078  linethru  26079  itg2addnc  26249  mzpcompact2lem  26799  2reu4  27935  el2wlksoton  28298  el2spthsoton  28299  n4cyclfrgra  28345  vdn0frgrav2  28351  vdgn0frgrav2  28352  vdn1frgrav2  28353  vdgn1frgrav2  28354  2spotmdisj  28394  isline  30473
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator