Theorem rexlimdvva 2658

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202   E.wrex 2511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  ovelrn  6171  f1o2ndf1  6393  eroveu  6795  eroprf  6797  genipv  7729  genpelvl  7732  genpelvu  7733  genprndl  7741  genprndu  7742  addlocpr  7756  addnqprlemrl  7777  addnqprlemru  7778  mulnqprlemrl  7793  mulnqprlemru  7794  ltsopr  7816  ltaddpr  7817  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  caucvgprlemdisj  7894  caucvgprlemladdfu  7897  caucvgprprlemdisj  7922  apreap  8767  apreim  8783  apirr  8785  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  apti  8802  aprcl  8826  qapne  9873  qtri3or  10501  exbtwnzlemex  10510  rebtwn2z  10515  cjap  11468  rexanre  11782  climcn2  11871  summodc  11946  prodmodclem2  12140  prodmodc  12141  eirrap  12341  dvds2lem  12366  bezoutlemnewy  12569  bezoutlembi  12578  dvdsmulgcd  12598  divgcdcoprm0  12675  cncongr1  12677  sqrt2irrap  12754  pcqmul  12878  pcneg  12900  pcadd  12915  4sqlem1  12963  4sqlem2  12964  4sqlem4  12967  mul4sq  12969  4sqlem12  12977  4sqlem13m  12978  4sqlem18  12983  imasaddfnlemg  13399  imasmnd2  13537  imasgrp2  13699  imasrng  13972  imasring  14080  dvdsrtr  14118  isnzr2  14201  lss1d  14400  znidom  14674  restbasg  14895  txbas  14985  blin2  15159  xmettxlem  15236  xmettx  15237  addcncntoplem  15288  mulcncf  15335  plyf  15464  plyadd  15478  plymul  15479  plyco  15486  plycj  15488  plycn  15489  plyrecj  15490  dvply2g  15493  logbgcd1irr  15694  logbgcd1irrap  15697  2sqlem5  15851  2sqlem9  15856  upgrpredgv  16000  usgredg4  16069  usgr1vr  16102