Theorem rexlimdvva 2676

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  ovelrn  6241  f1o2ndf1  6468  eroveu  6904  eroprf  6906  genipv  7882  genpelvl  7885  genpelvu  7886  genprndl  7894  genprndu  7895  addlocpr  7909  addnqprlemrl  7930  addnqprlemru  7931  mulnqprlemrl  7946  mulnqprlemru  7947  ltsopr  7969  ltaddpr  7970  ltexprlemfl  7982  ltexprlemrl  7983  ltexprlemfu  7984  ltexprlemru  7985  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  caucvgprlemdisj  8047  caucvgprlemladdfu  8050  caucvgprprlemdisj  8075  apreap  8923  apreim  8939  apirr  8941  apsym  8942  apcotr  8943  apadd1  8944  apneg  8947  mulext1  8948  apti  8958  aprcl  8982  qapne  10055  qtri3or  10692  exbtwnzlemex  10701  rebtwn2z  10706  cjap  11694  rexanre  12009  climcn2  12100  summodc  12175  prodmodclem2  12369  prodmodc  12370  eirrap  12570  dvds2lem  12595  bezoutlemnewy  12798  bezoutlembi  12807  dvdsmulgcd  12827  divgcdcoprm0  12904  cncongr1  12906  sqrt2irrap  12985  pcqmul  13111  pcneg  13133  pcadd  13148  4sqlem1  13196  4sqlem2  13197  4sqlem4  13200  mul4sq  13202  4sqlem12  13210  4sqlem13m  13211  4sqlem18  13216  imasaddfnlemg  13694  imasmnd2  13818  imasgrp2  13972  imasrng  14362  imasring  14478  dvdsrtr  14517  isnzr2  14600  lss1d  14829  znidom  15101  restbasg  15394  txbas  15484  blin2  15658  xmettxlem  15735  xmettx  15736  addcncntoplem  15787  mulcncf  15834  plyf  15963  plyadd  15977  plymul  15978  plyco  15985  plycj  15987  plycn  15988  plyrecj  15989  dvply2g  15992  logbgcd1irr  16203  logbgcd1irrap  16206  zprmlogbap  16218  2sqlem5  16443  2sqlem9  16448  upgrpredgv  16592  usgredg4  16661  usgr1vr  16694  qdiff  17305