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

Theorem rexlimivv 2706
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 2701 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2695 1  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1701   E.wrex 2578
This theorem is referenced by:  2reu5  3007  opelxp  4756  opiota  6332  tfrlem5  6438  xpdom2  7000  1sdom  7108  unxpdomlem3  7112  unfi  7169  elfiun  7228  xpnum  7629  kmlem9  7829  nqereu  8598  distrlem5pr  8696  mulid1  8880  1re  8882  mul02  9035  cnegex  9038  recex  9445  creur  9785  creui  9786  cju  9787  elz2  10087  zaddcl  10106  qre  10368  qaddcl  10379  qnegcl  10380  qmulcl  10381  qreccl  10383  replim  11648  xpnnenOLD  12535  odd2np1  12634  qredeu  12833  opoe  12911  omoe  12912  opeo  12913  omeo  12914  pythagtriplem1  12916  pcz  12980  4sqlem1  13042  4sqlem2  13043  4sqlem4  13046  mul4sq  13048  efgmnvl  15072  efgrelexlema  15107  txuni2  17316  tx2ndc  17401  blssioo  18353  tgioo  18354  ioorf  18981  ioorinv  18984  ioorcl  18985  dyaddisj  19004  mbfid  19044  elply  19630  vmacl  20409  efvmacl  20411  vmalelog  20497  2sqlem2  20656  mul2sq  20657  2sqlem7  20662  pntibnd  20795  ostth  20841  lpni  20899  ipasslem5  21468  ipasslem11  21473  hhssnv  21896  shscli  21951  shsleji  22004  shsidmi  22018  spansncvi  22286  superpos  22989  chirredi  23029  mdsymlem6  23043  rnmpt2ss  23236  cnre2csqima  23378  dya2icobrsiga  23800  dya2iocnrect  23805  dya2iocucvr  23808  sxbrsigalem2  23810  ghomgrpilem2  24277  prodmo  24439  poseq  24638  soseq  24639  nofulllem5  24745  elaltxp  24895  altxpsspw  24897  funtransport  25040  funray  25149  funline  25151  ellines  25161  linethru  25162  itg2addnc  25319  mzpcompact2lem  25977  2reu4  27116  n4cyclfrgra  27610  vdn0frgrav2  27616  vdgn0frgrav2  27617  vdn1frgrav2  27618  vdgn1frgrav2  27619  isline  29746
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-11 1732
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1533  df-nf 1536  df-ral 2582  df-rex 2583
  Copyright terms: Public domain W3C validator