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

Theorem rexlimdvva 2647
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 425 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ( ps  ->  ch ) ) )
32rexlimdvv 2646 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   E.wrex 2517
This theorem is referenced by:  disjxiun  3980  eroveu  6707  eroprf  6710  unxpdomlem3  7023  finsschain  7116  dffi3  7138  sornom  7857  genpv  8577  genpdm  8580  1re  8791  cnegex  8947  zaddcl  10012  rexanre  11781  o1lo1  11962  lo1resb  11989  o1resb  11991  rlimcn2  12015  climcn2  12017  o1of2  12037  o1rlimmul  12043  lo1add  12051  lo1mul  12052  summo  12141  o1fsum  12222  dvds2lem  12489  bezoutlem4  12668  dvdsmulgcd  12681  pcqmul  12854  pcneg  12874  pcadd  12885  4sqlem1  12943  4sqlem2  12944  4sqlem4  12947  mul4sq  12949  4sqlem12  12951  4sqlem13  12952  4sqlem18  12957  vdwmc2  12974  vdwlem7  12982  vdwlem9  12984  vdwlem10  12985  vdwlem11  12986  ramlb  13014  ramub1lem2  13022  imasaddfnlem  13378  imasmnd2  14357  imasgrp2  14558  gaorber  14710  lsmsubm  14912  lsmsubg  14913  lsmmod  14932  lsmdisj2  14939  pj1eu  14953  efgtlen  14983  efgredlem  15004  efgredeu  15009  efgcpbllemb  15012  frgpuptinv  15028  frgpup3lem  15034  divsabl  15105  frgpnabllem1  15109  frgpnabl  15111  cygabl  15125  dprdsubg  15207  ablfacrp  15249  pgpfac1lem3  15260  imasrng  15350  dvdsrtr  15382  lss1d  15668  lsmcl  15784  lsmelval2  15786  lbsextlem2  15860  isnzr2  15963  qsssubdrg  16379  znfld  16462  cygznlem3  16471  lsmcss  16540  restbas  16837  ordtbas2  16869  ordtbas  16870  cnhaus  17030  cldllycmp  17169  txbas  17210  ptbasin  17220  txcls  17247  xkoccn  17261  txindis  17276  txlly  17278  txnlly  17279  pthaus  17280  ptrescn  17281  txhaus  17289  tx1stc  17292  txkgen  17294  xkohaus  17295  xkoptsub  17296  xkopt  17297  xkoco1cn  17299  xkoco2cn  17300  xkoinjcn  17329  fmfnfmlem3  17599  fmfnfmlem4  17600  hausflimi  17623  hauspwpwf1  17630  txflf  17649  divstgplem  17751  blin2  17923  prdsxmslem2  18023  xrge0tsms  18287  addcnlem  18316  minveclem3b  18740  pmltpc  18758  evthicc2  18768  dyaddisj  18899  ismbfd  18943  mbfimaopnlem  18958  rolle  19285  dvcnvrelem1  19312  dvcvx  19315  itgsubst  19344  plyf  19528  plypf1  19542  plyadd  19547  plymul  19548  coeeu  19555  dgrlem  19559  coeid  19568  aalioulem6  19665  o1cxp  20217  dchrptlem2  20452  lgsdchr  20535  2sqlem5  20555  2sqlem9  20560  2sqb  20565  pntlemp  20707  pnt3  20709  ostthlem1  20724  ostth3  20735  ubthlem3  21397  cdjreui  22958  cdj3i  22967  txpcon  23121  cvmlift2lem10  23201  cvmlift2lem12  23203  cvmlift3lem7  23214  cvmlift3lem8  23215  br8  23470  br6  23471  br4  23472  axfelem20  23720  axcontlem4  23956  axcontlem9  23961  brsegle  24092  uninqs  24391  repcpwti  24514  tailfb  25679  isbnd2  25860  isbnd3  25861  ssbnd  25865  ispridlc  26048  ralxpmap  26114  eldioph2  26194  eldioph2b  26195  diophin  26205  diophun  26206  fphpdo  26253  irrapxlem3  26262  irrapxlem5  26264  pell1234qrne0  26291  pell1234qrreccl  26292  pell1234qrmulcl  26293  pell14qrgt0  26297  pell14qrdich  26307  pell1qrge1  26308  pell1qrgap  26312  pellqrex  26317  rmxycomplete  26355  jm2.27  26454  psgnunilem2  26771  psgneu  26782  psgnghm  26790  lshpkrlem6  28456  athgt  28796  3dim1  28807  3dim2  28808  lvolex3N  28878  llncvrlpln2  28897  lplncvrlvol2  28955  linepsubN  29092  lncvrelatN  29121  linepsubclN  29291
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2521  df-rex 2522
  Copyright terms: Public domain W3C validator