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

Theorem rexlimdvva 2636
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 2635 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 2510
This theorem is referenced by:  disjxiun  3917  eroveu  6639  eroprf  6642  unxpdomlem3  6954  finsschain  7046  dffi3  7068  sornom  7787  genpv  8503  genpdm  8506  1re  8717  cnegex  8873  zaddcl  9938  rexanre  11707  o1lo1  11888  lo1resb  11915  o1resb  11917  rlimcn2  11941  climcn2  11943  o1of2  11963  o1rlimmul  11969  lo1add  11977  lo1mul  11978  summo  12067  o1fsum  12148  dvds2lem  12415  bezoutlem4  12594  dvdsmulgcd  12607  pcqmul  12780  pcneg  12800  pcadd  12811  4sqlem1  12869  4sqlem2  12870  4sqlem4  12873  mul4sq  12875  4sqlem12  12877  4sqlem13  12878  4sqlem18  12883  vdwmc2  12900  vdwlem7  12908  vdwlem9  12910  vdwlem10  12911  vdwlem11  12912  ramlb  12940  ramub1lem2  12948  imasaddfnlem  13304  imasmnd2  14244  imasgrp2  14445  gaorber  14597  lsmsubm  14799  lsmsubg  14800  lsmmod  14819  lsmdisj2  14826  pj1eu  14840  efgtlen  14870  efgredlem  14891  efgredeu  14896  efgcpbllemb  14899  frgpuptinv  14915  frgpup3lem  14921  divsabl  14992  frgpnabllem1  14996  frgpnabl  14998  cygabl  15012  dprdsubg  15094  ablfacrp  15136  pgpfac1lem3  15147  imasrng  15237  dvdsrtr  15269  lss1d  15555  lsmcl  15671  lsmelval2  15673  lbsextlem2  15744  isnzr2  15847  qsssubdrg  16263  znfld  16346  cygznlem3  16355  lsmcss  16424  restbas  16721  ordtbas2  16753  ordtbas  16754  cnhaus  16914  cldllycmp  17053  txbas  17094  ptbasin  17104  txcls  17131  xkoccn  17145  txindis  17160  txlly  17162  txnlly  17163  pthaus  17164  ptrescn  17165  txhaus  17173  tx1stc  17176  txkgen  17178  xkohaus  17179  xkoptsub  17180  xkopt  17181  xkoco1cn  17183  xkoco2cn  17184  xkoinjcn  17213  fmfnfmlem3  17483  fmfnfmlem4  17484  hausflimi  17507  hauspwpwf1  17514  txflf  17533  divstgplem  17635  blin2  17807  prdsxmslem2  17907  xrge0tsms  18171  addcnlem  18200  minveclem3b  18624  pmltpc  18642  evthicc2  18652  dyaddisj  18783  ismbfd  18827  mbfimaopnlem  18842  rolle  19169  dvcnvrelem1  19196  dvcvx  19199  itgsubst  19228  plyf  19412  plypf1  19426  plyadd  19431  plymul  19432  coeeu  19439  dgrlem  19443  coeid  19452  aalioulem6  19549  o1cxp  20101  dchrptlem2  20336  lgsdchr  20419  2sqlem5  20439  2sqlem9  20444  2sqb  20449  pntlemp  20591  pnt3  20593  ostthlem1  20608  ostth3  20619  ubthlem3  21281  cdjreui  22842  cdj3i  22851  txpcon  22934  cvmlift2lem10  23014  cvmlift2lem12  23016  cvmlift3lem7  23027  cvmlift3lem8  23028  br8  23283  br6  23284  br4  23285  axfelem20  23533  axcontlem4  23769  axcontlem9  23774  brsegle  23905  uninqs  24204  repcpwti  24327  tailfb  25492  isbnd2  25673  isbnd3  25674  ssbnd  25678  ispridlc  25861  ralxpmap  25927  eldioph2  26007  eldioph2b  26008  diophin  26018  diophun  26019  fphpdo  26066  irrapxlem3  26075  irrapxlem5  26077  pell1234qrne0  26104  pell1234qrreccl  26105  pell1234qrmulcl  26106  pell14qrgt0  26110  pell14qrdich  26120  pell1qrge1  26121  pell1qrgap  26125  pellqrex  26130  rmxycomplete  26168  jm2.27  26267  psgnunilem2  26584  psgneu  26595  psgnghm  26603  lshpkrlem6  28209  athgt  28549  3dim1  28560  3dim2  28561  lvolex3N  28631  llncvrlpln2  28650  lplncvrlvol2  28708  linepsubN  28845  lncvrelatN  28874  linepsubclN  29044
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 2513  df-rex 2514
  Copyright terms: Public domain W3C validator