Theorem rexlimdvva 2924

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

Step	Hyp	Ref	Expression
1		rexlimdvva.1	. . 3 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps -> ch ) )
2	1	ex 435	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
3	2	rexlimdvv 2923	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1868   E.wrex 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2780  df-rex 2781

This theorem is referenced by:  disjxiun  4417  f1prex  6194  f1o2ndf1  6912  uniinqs  7448  eroveu  7463  eroprf  7466  ralxpmap  7526  unxpdomlem3  7781  finsschain  7884  dffi3  7948  sornom  8708  genpv  9425  genpdm  9428  1re  9643  cnegex  9815  zaddcl  10978  rexanre  13398  o1lo1  13589  lo1resb  13616  o1resb  13618  rlimcn2  13642  climcn2  13644  o1of2  13664  o1rlimmul  13670  lo1add  13678  lo1mul  13679  summo  13771  o1fsum  13861  ntrivcvgmul  13946  prodmolem2  13977  prodmo  13978  dvds2lem  14303  bezoutlem4OLD  14494  bezoutlem4  14497  dvdsmulgcd  14510  pcqmul  14791  pcneg  14811  pcadd  14822  4sqlem1  14880  4sqlem2  14881  4sqlem4  14884  mul4sq  14886  4sqlem12  14888  4sqlem13OLD  14889  4sqlem18OLD  14894  4sqlem13  14895  4sqlem18  14900  vdwmc2  14917  vdwlem7  14925  vdwlem9  14927  vdwlem10  14928  vdwlem11  14929  ramlb  14965  ramub1lem2  14973  imasaddfnlem  15422  imasmnd2  16561  imasgrp2  16789  gaorber  16950  psgnunilem2  17124  psgneu  17135  lsmsubm  17293  lsmsubg  17294  lsmmod  17313  lsmdisj2  17320  pj1eu  17334  efgtlen  17364  efgredlem  17385  efgredeu  17390  efgcpbllemb  17393  frgpuptinv  17409  frgpup3lem  17415  qusabl  17491  frgpnabllem1  17497  frgpnabl  17499  cygabl  17513  dprdsubg  17645  ablfacrp  17687  pgpfac1lem3  17698  imasring  17835  dvdsrtr  17868  lss1d  18174  lsmcl  18294  lsmelval2  18296  lbsextlem2  18370  isnzr2  18475  qsssubdrg  19015  znfld  19118  cygznlem3  19127  psgnghm  19135  lsmcss  19242  mdetunilem7  19630  mdetunilem8  19631  cayleyhamilton0  19900  cayleyhamiltonALT  19902  restbas  20161  ordtbas2  20194  ordtbas  20195  cnhaus  20357  cldllycmp  20497  txbas  20569  ptbasin  20579  txcls  20606  xkoccn  20621  txindis  20636  txlly  20638  txnlly  20639  pthaus  20640  ptrescn  20641  txhaus  20649  tx1stc  20652  txkgen  20654  xkohaus  20655  xkoptsub  20656  xkopt  20657  xkoco1cn  20659  xkoco2cn  20660  xkoinjcn  20689  fmfnfmlem3  20958  fmfnfmlem4  20959  hausflimi  20982  hauspwpwf1  20989  txflf  21008  qustgplem  21122  blin2  21431  prdsxmslem2  21531  xrge0tsms  21839  addcnlem  21883  minveclem3b  22357  minveclem3bOLD  22369  pmltpc  22388  evthicc2  22398  dyaddisj  22541  ismbfd  22583  mbfimaopnlem  22598  rolle  22929  dvcnvrelem1  22956  dvcvx  22959  itgsubst  22988  plyf  23139  plypf1  23153  plyadd  23158  plymul  23159  coeeu  23166  dgrlem  23170  coeid  23179  aalioulem6  23280  o1cxp  23887  dchrptlem2  24180  lgsdchr  24263  2sqlem5  24283  2sqlem9  24288  2sqb  24293  pntlemp  24435  pnt3  24437  ostthlem1  24452  ostth3  24463  axcontlem4  24984  axcontlem9  24989  sizeusglecusglem1  25198  el2wlksotot  25596  3cyclfrgra  25729  n4cyclfrgra  25732  frgrawopreg  25763  ubthlem3  26500  cdjreui  28071  cdj3i  28080  br8d  28208  xrofsup  28347  xrge0tsmsd  28544  qqhval2  28782  mbfmco2  29083  txpcon  29951  cvmlift2lem10  30031  cvmlift2lem12  30033  cvmlift3lem7  30044  cvmlift3lem8  30045  mclsppslem  30217  br8  30391  br6  30392  br4  30393  brsegle  30868  tailfb  31026  mblfinlem3  31893  ismblfin  31895  itg2addnc  31910  ftc1anc  31939  isbnd2  32029  isbnd3  32030  ssbnd  32034  ispridlc  32217  lshpkrlem6  32600  athgt  32940  3dim1  32951  3dim2  32952  lvolex3N  33022  llncvrlpln2  33041  lplncvrlvol2  33099  linepsubN  33236  lncvrelatN  33265  linepsubclN  33435  eldioph2  35523  eldioph2b  35524  diophin  35534  diophun  35535  fphpdo  35579  irrapxlem3  35588  irrapxlem5  35590  pell1234qrne0  35619  pell1234qrreccl  35620  pell1234qrmulcl  35621  pell14qrgt0  35625  pell14qrdich  35635  pell1qrge1  35636  pell1qrgap  35640  pellqrex  35646  rmxycomplete  35685  jm2.27  35783  stoweidlem49  37730  gbogt5  38575  usgredg4  38919  m1modmmod  39598