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  txpcon  23174  cvmlift2lem10  23254  cvmlift2lem12  23256  cvmlift3lem7  23267  cvmlift3lem8  23268  br8  23524  br6  23525  br4  23526  axcontlem4  24006  axcontlem9  24011  brsegle  24142  uninqs  24451  repcpwti  24573  tailfb  25738  isbnd2  25919  isbnd3  25920  ssbnd  25924  ispridlc  26107  ralxpmap  26173  eldioph2  26253  eldioph2b  26254  diophin  26264  diophun  26265  fphpdo  26312  irrapxlem3  26321  irrapxlem5  26323  pell1234qrne0  26350  pell1234qrreccl  26351  pell1234qrmulcl  26352  pell14qrgt0  26356  pell14qrdich  26366  pell1qrge1  26367  pell1qrgap  26371  pellqrex  26376  rmxycomplete  26414  jm2.27  26513  psgnunilem2  26830  psgneu  26841  psgnghm  26849  lshpkrlem6  28678  athgt  29018  3dim1  29029  3dim2  29030  lvolex3N  29100  llncvrlpln2  29119  lplncvrlvol2  29177  linepsubN  29314  lncvrelatN  29343  linepsubclN  29513
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