Theorem rexlimdvva 2942

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 434	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
3	2	rexlimdvv 2941	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1804   E.wrex 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-ral 2798  df-rex 2799

This theorem is referenced by:  disjxiun  4434  f1o2ndf1  6893  uniinqs  7393  eroveu  7408  eroprf  7411  ralxpmap  7470  unxpdomlem3  7728  finsschain  7829  dffi3  7893  sornom  8660  genpv  9380  genpdm  9383  1re  9598  cnegex  9764  zaddcl  10911  rexanre  13160  o1lo1  13341  lo1resb  13368  o1resb  13370  rlimcn2  13394  climcn2  13396  o1of2  13416  o1rlimmul  13422  lo1add  13430  lo1mul  13431  summo  13520  o1fsum  13608  ntrivcvgmul  13692  prodmolem2  13723  prodmo  13724  dvds2lem  13977  bezoutlem4  14160  dvdsmulgcd  14173  pcqmul  14358  pcneg  14378  pcadd  14389  4sqlem1  14447  4sqlem2  14448  4sqlem4  14451  mul4sq  14453  4sqlem12  14455  4sqlem13  14456  4sqlem18  14461  vdwmc2  14478  vdwlem7  14486  vdwlem9  14488  vdwlem10  14489  vdwlem11  14490  ramlb  14518  ramub1lem2  14526  imasaddfnlem  14906  imasmnd2  15935  imasgrp2  16163  gaorber  16324  psgnunilem2  16498  psgneu  16509  lsmsubm  16651  lsmsubg  16652  lsmmod  16671  lsmdisj2  16678  pj1eu  16692  efgtlen  16722  efgredlem  16743  efgredeu  16748  efgcpbllemb  16751  frgpuptinv  16767  frgpup3lem  16773  qusabl  16849  frgpnabllem1  16855  frgpnabl  16857  cygabl  16871  dprdsubg  17049  ablfacrp  17095  pgpfac1lem3  17106  imasring  17246  dvdsrtr  17279  lss1d  17587  lsmcl  17707  lsmelval2  17709  lbsextlem2  17783  isnzr2  17889  qsssubdrg  18455  znfld  18576  cygznlem3  18585  psgnghm  18593  lsmcss  18700  mdetunilem7  19097  mdetunilem8  19098  cayleyhamilton0  19367  cayleyhamiltonALT  19369  restbas  19636  ordtbas2  19669  ordtbas  19670  cnhaus  19832  cldllycmp  19973  txbas  20045  ptbasin  20055  txcls  20082  xkoccn  20097  txindis  20112  txlly  20114  txnlly  20115  pthaus  20116  ptrescn  20117  txhaus  20125  tx1stc  20128  txkgen  20130  xkohaus  20131  xkoptsub  20132  xkopt  20133  xkoco1cn  20135  xkoco2cn  20136  xkoinjcn  20165  fmfnfmlem3  20434  fmfnfmlem4  20435  hausflimi  20458  hauspwpwf1  20465  txflf  20484  qustgplem  20596  blin2  20909  prdsxmslem2  21009  xrge0tsms  21316  addcnlem  21345  minveclem3b  21820  pmltpc  21839  evthicc2  21849  dyaddisj  21982  ismbfd  22024  mbfimaopnlem  22039  rolle  22368  dvcnvrelem1  22395  dvcvx  22398  itgsubst  22427  plyf  22572  plypf1  22586  plyadd  22591  plymul  22592  coeeu  22599  dgrlem  22603  coeid  22612  aalioulem6  22709  o1cxp  23280  dchrptlem2  23516  lgsdchr  23599  2sqlem5  23619  2sqlem9  23624  2sqb  23629  pntlemp  23771  pnt3  23773  ostthlem1  23788  ostth3  23799  axcontlem4  24246  axcontlem9  24251  sizeusglecusglem1  24460  el2wlksotot  24858  3cyclfrgra  24991  n4cyclfrgra  24994  frgrawopreg  25025  ubthlem3  25764  cdjreui  27327  cdj3i  27336  br8d  27439  xrofsup  27558  xrge0tsmsd  27752  qqhval2  27940  mbfmco2  28213  txpcon  28654  cvmlift2lem10  28734  cvmlift2lem12  28736  cvmlift3lem7  28747  cvmlift3lem8  28748  mclsppslem  28920  br8  29160  br6  29161  br4  29162  brsegle  29733  mblfinlem3  30028  ismblfin  30030  itg2addnc  30044  ftc1anc  30073  tailfb  30170  isbnd2  30254  isbnd3  30255  ssbnd  30259  ispridlc  30442  eldioph2  30670  eldioph2b  30671  diophin  30681  diophun  30682  fphpdo  30726  irrapxlem3  30735  irrapxlem5  30737  pell1234qrne0  30764  pell1234qrreccl  30765  pell1234qrmulcl  30766  pell14qrgt0  30770  pell14qrdich  30780  pell1qrge1  30781  pell1qrgap  30785  pellqrex  30790  rmxycomplete  30828  jm2.27  30925  stoweidlem49  31720  lshpkrlem6  34580  athgt  34920  3dim1  34931  3dim2  34932  lvolex3N  35002  llncvrlpln2  35021  lplncvrlvol2  35079  linepsubN  35216  lncvrelatN  35245  linepsubclN  35415