Theorem rexlimdvva 2670

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

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

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 2527  df-rex 2528

This theorem is referenced by:  ovelrn  6211  f1o2ndf1  6437  eroveu  6873  eroprf  6875  genipv  7840  genpelvl  7843  genpelvu  7844  genprndl  7852  genprndu  7853  addlocpr  7867  addnqprlemrl  7888  addnqprlemru  7889  mulnqprlemrl  7904  mulnqprlemru  7905  ltsopr  7927  ltaddpr  7928  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  caucvgprlemdisj  8005  caucvgprlemladdfu  8008  caucvgprprlemdisj  8033  apreap  8878  apreim  8894  apirr  8896  apsym  8897  apcotr  8898  apadd1  8899  apneg  8902  mulext1  8903  apti  8913  aprcl  8937  qapne  9989  qtri3or  10624  exbtwnzlemex  10633  rebtwn2z  10638  cjap  11616  rexanre  11930  climcn2  12019  summodc  12094  prodmodclem2  12288  prodmodc  12289  eirrap  12489  dvds2lem  12514  bezoutlemnewy  12717  bezoutlembi  12726  dvdsmulgcd  12746  divgcdcoprm0  12823  cncongr1  12825  sqrt2irrap  12902  pcqmul  13026  pcneg  13048  pcadd  13063  4sqlem1  13111  4sqlem2  13112  4sqlem4  13115  mul4sq  13117  4sqlem12  13125  4sqlem13m  13126  4sqlem18  13131  imasaddfnlemg  13578  imasmnd2  13707  imasgrp2  13863  imasrng  14195  imasring  14307  dvdsrtr  14346  isnzr2  14429  lss1d  14657  znidom  14931  restbasg  15159  txbas  15249  blin2  15423  xmettxlem  15500  xmettx  15501  addcncntoplem  15552  mulcncf  15599  plyf  15728  plyadd  15742  plymul  15743  plyco  15750  plycj  15752  plycn  15753  plyrecj  15754  dvply2g  15757  logbgcd1irr  15958  logbgcd1irrap  15961  2sqlem5  16118  2sqlem9  16123  upgrpredgv  16267  usgredg4  16336  usgr1vr  16369  qdiff  16959