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

Theorem rexlimdvva 2674
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rexlimdvva.1  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  ->  ch ) )
Assertion
Ref Expression
rexlimdvva  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Distinct variable groups:    x, y, ph    ch, x, y    y, A
Allowed substitution hints:    ps( x, y)    A( x)    B( x, y)

Proof of Theorem rexlimdvva
StepHypRef Expression
1 rexlimdvva.1 . . 3  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  ->  ch ) )
21ex 423 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ( ps  ->  ch ) ) )
32rexlimdvv 2673 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  disjxiun  4020  eroveu  6753  eroprf  6756  unxpdomlem3  7069  finsschain  7162  dffi3  7184  sornom  7903  genpv  8623  genpdm  8626  1re  8837  cnegex  8993  zaddcl  10059  rexanre  11830  o1lo1  12011  lo1resb  12038  o1resb  12040  rlimcn2  12064  climcn2  12066  o1of2  12086  o1rlimmul  12092  lo1add  12100  lo1mul  12101  summo  12190  o1fsum  12271  dvds2lem  12541  bezoutlem4  12720  dvdsmulgcd  12733  pcqmul  12906  pcneg  12926  pcadd  12937  4sqlem1  12995  4sqlem2  12996  4sqlem4  12999  mul4sq  13001  4sqlem12  13003  4sqlem13  13004  4sqlem18  13009  vdwmc2  13026  vdwlem7  13034  vdwlem9  13036  vdwlem10  13037  vdwlem11  13038  ramlb  13066  ramub1lem2  13074  imasaddfnlem  13430  imasmnd2  14409  imasgrp2  14610  gaorber  14762  lsmsubm  14964  lsmsubg  14965  lsmmod  14984  lsmdisj2  14991  pj1eu  15005  efgtlen  15035  efgredlem  15056  efgredeu  15061  efgcpbllemb  15064  frgpuptinv  15080  frgpup3lem  15086  divsabl  15157  frgpnabllem1  15161  frgpnabl  15163  cygabl  15177  dprdsubg  15259  ablfacrp  15301  pgpfac1lem3  15312  imasrng  15402  dvdsrtr  15434  lss1d  15720  lsmcl  15836  lsmelval2  15838  lbsextlem2  15912  isnzr2  16015  qsssubdrg  16431  znfld  16514  cygznlem3  16523  lsmcss  16592  restbas  16889  ordtbas2  16921  ordtbas  16922  cnhaus  17082  cldllycmp  17221  txbas  17262  ptbasin  17272  txcls  17299  xkoccn  17313  txindis  17328  txlly  17330  txnlly  17331  pthaus  17332  ptrescn  17333  txhaus  17341  tx1stc  17344  txkgen  17346  xkohaus  17347  xkoptsub  17348  xkopt  17349  xkoco1cn  17351  xkoco2cn  17352  xkoinjcn  17381  fmfnfmlem3  17651  fmfnfmlem4  17652  hausflimi  17675  hauspwpwf1  17682  txflf  17701  divstgplem  17803  blin2  17975  prdsxmslem2  18075  xrge0tsms  18339  addcnlem  18368  minveclem3b  18792  pmltpc  18810  evthicc2  18820  dyaddisj  18951  ismbfd  18995  mbfimaopnlem  19010  rolle  19337  dvcnvrelem1  19364  dvcvx  19367  itgsubst  19396  plyf  19580  plypf1  19594  plyadd  19599  plymul  19600  coeeu  19607  dgrlem  19611  coeid  19620  aalioulem6  19717  o1cxp  20269  dchrptlem2  20504  lgsdchr  20587  2sqlem5  20607  2sqlem9  20612  2sqb  20617  pntlemp  20759  pnt3  20761  ostthlem1  20776  ostth3  20787  ubthlem3  21451  cdjreui  23012  cdj3i  23021  xrge0tsmsd  23382  mbfmco2  23570  txpcon  23763  cvmlift2lem10  23843  cvmlift2lem12  23845  cvmlift3lem7  23856  cvmlift3lem8  23857  br8  24113  br6  24114  br4  24115  axcontlem4  24595  axcontlem9  24600  brsegle  24731  uninqs  25039  repcpwti  25161  tailfb  26326  isbnd2  26507  isbnd3  26508  ssbnd  26512  ispridlc  26695  ralxpmap  26761  eldioph2  26841  eldioph2b  26842  diophin  26852  diophun  26853  fphpdo  26900  irrapxlem3  26909  irrapxlem5  26911  pell1234qrne0  26938  pell1234qrreccl  26939  pell1234qrmulcl  26940  pell14qrgt0  26944  pell14qrdich  26954  pell1qrge1  26955  pell1qrgap  26959  pellqrex  26964  rmxycomplete  27002  jm2.27  27101  psgnunilem2  27418  psgneu  27429  psgnghm  27437  lshpkrlem6  29305  athgt  29645  3dim1  29656  3dim2  29657  lvolex3N  29727  llncvrlpln2  29746  lplncvrlvol2  29804  linepsubN  29941  lncvrelatN  29970  linepsubclN  30140
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator