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  6238  f1o2ndf1  6464  eroveu  6900  eroprf  6902  genipv  7876  genpelvl  7879  genpelvu  7880  genprndl  7888  genprndu  7889  addlocpr  7903  addnqprlemrl  7924  addnqprlemru  7925  mulnqprlemrl  7940  mulnqprlemru  7941  ltsopr  7963  ltaddpr  7964  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  caucvgprlemdisj  8041  caucvgprlemladdfu  8044  caucvgprprlemdisj  8069  apreap  8917  apreim  8933  apirr  8935  apsym  8936  apcotr  8937  apadd1  8938  apneg  8941  mulext1  8942  apti  8952  aprcl  8976  qapne  10048  qtri3or  10685  exbtwnzlemex  10694  rebtwn2z  10699  cjap  11686  rexanre  12001  climcn2  12091  summodc  12166  prodmodclem2  12360  prodmodc  12361  eirrap  12561  dvds2lem  12586  bezoutlemnewy  12789  bezoutlembi  12798  dvdsmulgcd  12818  divgcdcoprm0  12895  cncongr1  12897  sqrt2irrap  12976  pcqmul  13102  pcneg  13124  pcadd  13139  4sqlem1  13187  4sqlem2  13188  4sqlem4  13191  mul4sq  13193  4sqlem12  13201  4sqlem13m  13202  4sqlem18  13207  imasaddfnlemg  13684  imasmnd2  13808  imasgrp2  13962  imasrng  14304  imasring  14418  dvdsrtr  14457  isnzr2  14540  lss1d  14769  znidom  15041  restbasg  15318  txbas  15408  blin2  15582  xmettxlem  15659  xmettx  15660  addcncntoplem  15711  mulcncf  15758  plyf  15887  plyadd  15901  plymul  15902  plyco  15909  plycj  15911  plycn  15912  plyrecj  15913  dvply2g  15916  logbgcd1irr  16122  logbgcd1irrap  16125  zprmlogbap  16137  2sqlem5  16336  2sqlem9  16341  upgrpredgv  16485  usgredg4  16554  usgr1vr  16587  qdiff  17196