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

Theorem rexlimdvva 2675
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 2674 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 1685   E.wrex 2545
This theorem is referenced by:  disjxiun  4021  eroveu  6748  eroprf  6751  unxpdomlem3  7064  finsschain  7157  dffi3  7179  sornom  7898  genpv  8618  genpdm  8621  1re  8832  cnegex  8988  zaddcl  10054  rexanre  11824  o1lo1  12005  lo1resb  12032  o1resb  12034  rlimcn2  12058  climcn2  12060  o1of2  12080  o1rlimmul  12086  lo1add  12094  lo1mul  12095  summo  12184  o1fsum  12265  dvds2lem  12535  bezoutlem4  12714  dvdsmulgcd  12727  pcqmul  12900  pcneg  12920  pcadd  12931  4sqlem1  12989  4sqlem2  12990  4sqlem4  12993  mul4sq  12995  4sqlem12  12997  4sqlem13  12998  4sqlem18  13003  vdwmc2  13020  vdwlem7  13028  vdwlem9  13030  vdwlem10  13031  vdwlem11  13032  ramlb  13060  ramub1lem2  13068  imasaddfnlem  13424  imasmnd2  14403  imasgrp2  14604  gaorber  14756  lsmsubm  14958  lsmsubg  14959  lsmmod  14978  lsmdisj2  14985  pj1eu  14999  efgtlen  15029  efgredlem  15050  efgredeu  15055  efgcpbllemb  15058  frgpuptinv  15074  frgpup3lem  15080  divsabl  15151  frgpnabllem1  15155  frgpnabl  15157  cygabl  15171  dprdsubg  15253  ablfacrp  15295  pgpfac1lem3  15306  imasrng  15396  dvdsrtr  15428  lss1d  15714  lsmcl  15830  lsmelval2  15832  lbsextlem2  15906  isnzr2  16009  qsssubdrg  16425  znfld  16508  cygznlem3  16517  lsmcss  16586  restbas  16883  ordtbas2  16915  ordtbas  16916  cnhaus  17076  cldllycmp  17215  txbas  17256  ptbasin  17266  txcls  17293  xkoccn  17307  txindis  17322  txlly  17324  txnlly  17325  pthaus  17326  ptrescn  17327  txhaus  17335  tx1stc  17338  txkgen  17340  xkohaus  17341  xkoptsub  17342  xkopt  17343  xkoco1cn  17345  xkoco2cn  17346  xkoinjcn  17375  fmfnfmlem3  17645  fmfnfmlem4  17646  hausflimi  17669  hauspwpwf1  17676  txflf  17695  divstgplem  17797  blin2  17969  prdsxmslem2  18069  xrge0tsms  18333  addcnlem  18362  minveclem3b  18786  pmltpc  18804  evthicc2  18814  dyaddisj  18945  ismbfd  18989  mbfimaopnlem  19004  rolle  19331  dvcnvrelem1  19358  dvcvx  19361  itgsubst  19390  plyf  19574  plypf1  19588  plyadd  19593  plymul  19594  coeeu  19601  dgrlem  19605  coeid  19614  aalioulem6  19711  o1cxp  20263  dchrptlem2  20498  lgsdchr  20581  2sqlem5  20601  2sqlem9  20606  2sqb  20611  pntlemp  20753  pnt3  20755  ostthlem1  20770  ostth3  20781  ubthlem3  21443  cdjreui  23004  cdj3i  23013  txpcon  23167  cvmlift2lem10  23247  cvmlift2lem12  23249  cvmlift3lem7  23260  cvmlift3lem8  23261  br8  23516  br6  23517  br4  23518  axfelem20  23766  axcontlem4  24002  axcontlem9  24007  brsegle  24138  uninqs  24437  repcpwti  24560  tailfb  25725  isbnd2  25906  isbnd3  25907  ssbnd  25911  ispridlc  26094  ralxpmap  26160  eldioph2  26240  eldioph2b  26241  diophin  26251  diophun  26252  fphpdo  26299  irrapxlem3  26308  irrapxlem5  26310  pell1234qrne0  26337  pell1234qrreccl  26338  pell1234qrmulcl  26339  pell14qrgt0  26343  pell14qrdich  26353  pell1qrge1  26354  pell1qrgap  26358  pellqrex  26363  rmxycomplete  26401  jm2.27  26500  psgnunilem2  26817  psgneu  26828  psgnghm  26836  lshpkrlem6  28572  athgt  28912  3dim1  28923  3dim2  28924  lvolex3N  28994  llncvrlpln2  29013  lplncvrlvol2  29071  linepsubN  29208  lncvrelatN  29237  linepsubclN  29407
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-nf 1533  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator