Theorem rexlimdvva 2658

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  ovelrn  6170  f1o2ndf1  6392  eroveu  6794  eroprf  6796  genipv  7728  genpelvl  7731  genpelvu  7732  genprndl  7740  genprndu  7741  addlocpr  7755  addnqprlemrl  7776  addnqprlemru  7777  mulnqprlemrl  7792  mulnqprlemru  7793  ltsopr  7815  ltaddpr  7816  ltexprlemfl  7828  ltexprlemrl  7829  ltexprlemfu  7830  ltexprlemru  7831  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  caucvgprlemdisj  7893  caucvgprlemladdfu  7896  caucvgprprlemdisj  7921  apreap  8766  apreim  8782  apirr  8784  apsym  8785  apcotr  8786  apadd1  8787  apneg  8790  mulext1  8791  apti  8801  aprcl  8825  qapne  9872  qtri3or  10499  exbtwnzlemex  10508  rebtwn2z  10513  cjap  11466  rexanre  11780  climcn2  11869  summodc  11943  prodmodclem2  12137  prodmodc  12138  eirrap  12338  dvds2lem  12363  bezoutlemnewy  12566  bezoutlembi  12575  dvdsmulgcd  12595  divgcdcoprm0  12672  cncongr1  12674  sqrt2irrap  12751  pcqmul  12875  pcneg  12897  pcadd  12912  4sqlem1  12960  4sqlem2  12961  4sqlem4  12964  mul4sq  12966  4sqlem12  12974  4sqlem13m  12975  4sqlem18  12980  imasaddfnlemg  13396  imasmnd2  13534  imasgrp2  13696  imasrng  13968  imasring  14076  dvdsrtr  14114  isnzr2  14197  lss1d  14396  znidom  14670  restbasg  14891  txbas  14981  blin2  15155  xmettxlem  15232  xmettx  15233  addcncntoplem  15284  mulcncf  15331  plyf  15460  plyadd  15474  plymul  15475  plyco  15482  plycj  15484  plycn  15485  plyrecj  15486  dvply2g  15489  logbgcd1irr  15690  logbgcd1irrap  15693  2sqlem5  15847  2sqlem9  15852  upgrpredgv  15996  usgredg4  16065  usgr1vr  16098