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

Theorem rexlimivv 2884
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 2879 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2873 1  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    e. wcel 1887   E.wrex 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-ral 2742  df-rex 2743
This theorem is referenced by:  2reu5  3248  opelxp  4864  opiota  6852  f1o2ndf1  6904  tfrlem5  7098  xpdom2  7667  1sdom  7775  unxpdomlem3  7778  unfi  7838  elfiun  7944  xpnum  8385  kmlem9  8588  nqereu  9354  distrlem5pr  9452  mulid1  9640  1re  9642  mul02  9811  cnegex  9814  recex  10244  creur  10603  creui  10604  cju  10605  elz2  10954  zaddcl  10977  qre  11269  qaddcl  11280  qnegcl  11281  qmulcl  11282  qreccl  11284  hash2prd  12634  elss2prb  12643  replim  13179  prodmo  13990  odd2np1  14365  qredeu  14664  opoe  14761  omoe  14762  opeo  14763  omeo  14764  pythagtriplem1  14766  pcz  14830  4sqlem1  14892  4sqlem2  14893  4sqlem4  14896  mul4sq  14898  pmtr3ncom  17116  efgmnvl  17364  efgrelexlema  17399  ring1ne0  17821  txuni2  20580  tx2ndc  20666  blssioo  21813  tgioo  21814  ioorf  22525  ioorinv  22528  ioorcl  22529  ioorfOLD  22530  ioorinvOLD  22533  ioorclOLD  22534  dyaddisj  22554  mbfid  22592  elply  23149  vmacl  24045  efvmacl  24047  vmalelog  24133  2sqlem2  24292  mul2sq  24293  2sqlem7  24298  pntibnd  24431  ostth  24477  legval  24629  usgrasscusgra  25211  el2wlksoton  25606  el2spthsoton  25607  n4cyclfrgra  25746  vdn0frgrav2  25751  vdgn0frgrav2  25752  vdn1frgrav2  25753  vdgn1frgrav2  25754  2spotmdisj  25796  friendshipgt3  25849  lpni  25911  ipasslem5  26476  ipasslem11  26481  hhssnv  26915  shscli  26970  shsleji  27023  shsidmi  27037  spansncvi  27305  superpos  28007  chirredi  28047  mdsymlem6  28061  rnmpt2ss  28276  cnre2csqima  28717  dya2icobrsiga  29098  dya2iocnrect  29103  dya2iocucvr  29106  sxbrsigalem2  29108  afsval  29488  msubco  30169  ghomgrpilem2  30304  poseq  30491  soseq  30492  nofulllem5  30595  elaltxp  30742  altxpsspw  30744  funtransport  30798  funray  30907  funline  30909  ellines  30919  linethru  30920  icoreresf  31755  icoreclin  31760  relowlssretop  31766  relowlpssretop  31767  itg2addnc  31996  isline  33304  mzpcompact2lem  35593  2reu4  38611  nnsum3primesgbe  38887  nnsum4primesodd  38891  nnsum4primesoddALTV  38892  fundmge2nop  39026  upgredgpr  39232  cusgredg  39492  usgredgsscusgredg  39520  usgvincvad  39769  usgvincvadALT  39772  nnpw2pb  40451
  Copyright terms: Public domain W3C validator