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  8915  apreim  8931  apirr  8933  apsym  8934  apcotr  8935  apadd1  8936  apneg  8939  mulext1  8940  apti  8950  aprcl  8974  qapne  10039  qtri3or  10675  exbtwnzlemex  10684  rebtwn2z  10689  cjap  11672  rexanre  11986  climcn2  12075  summodc  12150  prodmodclem2  12344  prodmodc  12345  eirrap  12545  dvds2lem  12570  bezoutlemnewy  12773  bezoutlembi  12782  dvdsmulgcd  12802  divgcdcoprm0  12879  cncongr1  12881  sqrt2irrap  12958  pcqmul  13082  pcneg  13104  pcadd  13119  4sqlem1  13167  4sqlem2  13168  4sqlem4  13171  mul4sq  13173  4sqlem12  13181  4sqlem13m  13182  4sqlem18  13187  imasaddfnlemg  13635  imasmnd2  13759  imasgrp2  13913  imasrng  14255  imasring  14369  dvdsrtr  14408  isnzr2  14491  lss1d  14720  znidom  14992  restbasg  15269  txbas  15359  blin2  15533  xmettxlem  15610  xmettx  15611  addcncntoplem  15662  mulcncf  15709  plyf  15838  plyadd  15852  plymul  15853  plyco  15860  plycj  15862  plycn  15863  plyrecj  15864  dvply2g  15867  logbgcd1irr  16069  logbgcd1irrap  16072  2sqlem5  16238  2sqlem9  16243  upgrpredgv  16387  usgredg4  16456  usgr1vr  16489  qdiff  17098