Theorem rexlimdvva 2668

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

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

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 2525  df-rex 2526

This theorem is referenced by:  ovelrn  6203  f1o2ndf1  6424  eroveu  6860  eroprf  6862  genipv  7824  genpelvl  7827  genpelvu  7828  genprndl  7836  genprndu  7837  addlocpr  7851  addnqprlemrl  7872  addnqprlemru  7873  mulnqprlemrl  7888  mulnqprlemru  7889  ltsopr  7911  ltaddpr  7912  ltexprlemfl  7924  ltexprlemrl  7925  ltexprlemfu  7926  ltexprlemru  7927  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  caucvgprlemdisj  7989  caucvgprlemladdfu  7992  caucvgprprlemdisj  8017  apreap  8861  apreim  8877  apirr  8879  apsym  8880  apcotr  8881  apadd1  8882  apneg  8885  mulext1  8886  apti  8896  aprcl  8920  qapne  9971  qtri3or  10600  exbtwnzlemex  10609  rebtwn2z  10614  cjap  11591  rexanre  11905  climcn2  11994  summodc  12069  prodmodclem2  12263  prodmodc  12264  eirrap  12464  dvds2lem  12489  bezoutlemnewy  12692  bezoutlembi  12701  dvdsmulgcd  12721  divgcdcoprm0  12798  cncongr1  12800  sqrt2irrap  12877  pcqmul  13001  pcneg  13023  pcadd  13038  4sqlem1  13086  4sqlem2  13087  4sqlem4  13090  mul4sq  13092  4sqlem12  13100  4sqlem13m  13101  4sqlem18  13106  imasaddfnlemg  13527  imasmnd2  13665  imasgrp2  13827  imasrng  14100  imasring  14208  dvdsrtr  14246  isnzr2  14329  lss1d  14531  znidom  14805  restbasg  15033  txbas  15123  blin2  15297  xmettxlem  15374  xmettx  15375  addcncntoplem  15426  mulcncf  15473  plyf  15602  plyadd  15616  plymul  15617  plyco  15624  plycj  15626  plycn  15627  plyrecj  15628  dvply2g  15631  logbgcd1irr  15832  logbgcd1irrap  15835  2sqlem5  15992  2sqlem9  15997  upgrpredgv  16141  usgredg4  16210  usgr1vr  16243  qdiff  16833