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 ) )

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

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

This theorem is referenced by:  ovelrn  6228  f1o2ndf1  6454  eroveu  6890  eroprf  6892  genipv  7866  genpelvl  7869  genpelvu  7870  genprndl  7878  genprndu  7879  addlocpr  7893  addnqprlemrl  7914  addnqprlemru  7915  mulnqprlemrl  7930  mulnqprlemru  7931  ltsopr  7953  ltaddpr  7954  ltexprlemfl  7966  ltexprlemrl  7967  ltexprlemfu  7968  ltexprlemru  7969  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  caucvgprlemdisj  8031  caucvgprlemladdfu  8034  caucvgprprlemdisj  8059  apreap  8905  apreim  8921  apirr  8923  apsym  8924  apcotr  8925  apadd1  8926  apneg  8929  mulext1  8930  apti  8940  aprcl  8964  qapne  10018  qtri3or  10653  exbtwnzlemex  10662  rebtwn2z  10667  cjap  11650  rexanre  11964  climcn2  12053  summodc  12128  prodmodclem2  12322  prodmodc  12323  eirrap  12523  dvds2lem  12548  bezoutlemnewy  12751  bezoutlembi  12760  dvdsmulgcd  12780  divgcdcoprm0  12857  cncongr1  12859  sqrt2irrap  12936  pcqmul  13060  pcneg  13082  pcadd  13097  4sqlem1  13145  4sqlem2  13146  4sqlem4  13149  mul4sq  13151  4sqlem12  13159  4sqlem13m  13160  4sqlem18  13165  imasaddfnlemg  13612  imasmnd2  13736  imasgrp2  13890  imasrng  14230  imasring  14342  dvdsrtr  14381  isnzr2  14464  lss1d  14692  znidom  14964  restbasg  15192  txbas  15282  blin2  15456  xmettxlem  15533  xmettx  15534  addcncntoplem  15585  mulcncf  15632  plyf  15761  plyadd  15775  plymul  15776  plyco  15783  plycj  15785  plycn  15786  plyrecj  15787  dvply2g  15790  logbgcd1irr  15992  logbgcd1irrap  15995  2sqlem5  16152  2sqlem9  16157  upgrpredgv  16301  usgredg4  16370  usgr1vr  16403  qdiff  17003