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  7877  genpelvl  7880  genpelvu  7881  genprndl  7889  genprndu  7890  addlocpr  7904  addnqprlemrl  7925  addnqprlemru  7926  mulnqprlemrl  7941  mulnqprlemru  7942  ltsopr  7964  ltaddpr  7965  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  caucvgprlemdisj  8042  caucvgprlemladdfu  8045  caucvgprprlemdisj  8070  apreap  8918  apreim  8934  apirr  8936  apsym  8937  apcotr  8938  apadd1  8939  apneg  8942  mulext1  8943  apti  8953  aprcl  8977  qapne  10049  qtri3or  10686  exbtwnzlemex  10695  rebtwn2z  10700  cjap  11688  rexanre  12003  climcn2  12094  summodc  12169  prodmodclem2  12363  prodmodc  12364  eirrap  12564  dvds2lem  12589  bezoutlemnewy  12792  bezoutlembi  12801  dvdsmulgcd  12821  divgcdcoprm0  12898  cncongr1  12900  sqrt2irrap  12979  pcqmul  13105  pcneg  13127  pcadd  13142  4sqlem1  13190  4sqlem2  13191  4sqlem4  13194  mul4sq  13196  4sqlem12  13204  4sqlem13m  13205  4sqlem18  13210  imasaddfnlemg  13688  imasmnd2  13812  imasgrp2  13966  imasrng  14339  imasring  14453  dvdsrtr  14492  isnzr2  14575  lss1d  14804  znidom  15076  restbasg  15360  txbas  15450  blin2  15624  xmettxlem  15701  xmettx  15702  addcncntoplem  15753  mulcncf  15800  plyf  15929  plyadd  15943  plymul  15944  plyco  15951  plycj  15953  plycn  15954  plyrecj  15955  dvply2g  15958  logbgcd1irr  16164  logbgcd1irrap  16167  zprmlogbap  16179  2sqlem5  16404  2sqlem9  16409  upgrpredgv  16553  usgredg4  16622  usgr1vr  16655  qdiff  17265