Theorem rexlimdvva 2659

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 2658	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516  df-rex 2517

This theorem is referenced by:  ovelrn  6181  f1o2ndf1  6402  eroveu  6838  eroprf  6840  genipv  7772  genpelvl  7775  genpelvu  7776  genprndl  7784  genprndu  7785  addlocpr  7799  addnqprlemrl  7820  addnqprlemru  7821  mulnqprlemrl  7836  mulnqprlemru  7837  ltsopr  7859  ltaddpr  7860  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  caucvgprlemdisj  7937  caucvgprlemladdfu  7940  caucvgprprlemdisj  7965  apreap  8809  apreim  8825  apirr  8827  apsym  8828  apcotr  8829  apadd1  8830  apneg  8833  mulext1  8834  apti  8844  aprcl  8868  qapne  9917  qtri3or  10546  exbtwnzlemex  10555  rebtwn2z  10560  cjap  11529  rexanre  11843  climcn2  11932  summodc  12007  prodmodclem2  12201  prodmodc  12202  eirrap  12402  dvds2lem  12427  bezoutlemnewy  12630  bezoutlembi  12639  dvdsmulgcd  12659  divgcdcoprm0  12736  cncongr1  12738  sqrt2irrap  12815  pcqmul  12939  pcneg  12961  pcadd  12976  4sqlem1  13024  4sqlem2  13025  4sqlem4  13028  mul4sq  13030  4sqlem12  13038  4sqlem13m  13039  4sqlem18  13044  imasaddfnlemg  13460  imasmnd2  13598  imasgrp2  13760  imasrng  14033  imasring  14141  dvdsrtr  14179  isnzr2  14262  lss1d  14462  znidom  14736  restbasg  14962  txbas  15052  blin2  15226  xmettxlem  15303  xmettx  15304  addcncntoplem  15355  mulcncf  15402  plyf  15531  plyadd  15545  plymul  15546  plyco  15553  plycj  15555  plycn  15556  plyrecj  15557  dvply2g  15560  logbgcd1irr  15761  logbgcd1irrap  15764  2sqlem5  15921  2sqlem9  15926  upgrpredgv  16070  usgredg4  16139  usgr1vr  16172  qdiff  16764