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  6241  f1o2ndf1  6468  eroveu  6905  eroprf  6907  genipv  7882  genpelvl  7885  genpelvu  7886  genprndl  7894  genprndu  7895  addlocpr  7909  addnqprlemrl  7930  addnqprlemru  7931  mulnqprlemrl  7946  mulnqprlemru  7947  ltsopr  7969  ltaddpr  7970  ltexprlemfl  7982  ltexprlemrl  7983  ltexprlemfu  7984  ltexprlemru  7985  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  caucvgprlemdisj  8047  caucvgprlemladdfu  8050  caucvgprprlemdisj  8075  apreap  8923  apreim  8939  apirr  8941  apsym  8942  apcotr  8943  apadd1  8944  apneg  8947  mulext1  8948  apti  8958  aprcl  8982  qapne  10054  qtri3or  10691  exbtwnzlemex  10700  rebtwn2z  10705  cjap  11693  rexanre  12008  climcn2  12099  summodc  12174  prodmodclem2  12368  prodmodc  12369  eirrap  12569  dvds2lem  12594  bezoutlemnewy  12797  bezoutlembi  12806  dvdsmulgcd  12826  divgcdcoprm0  12903  cncongr1  12905  sqrt2irrap  12984  pcqmul  13110  pcneg  13132  pcadd  13147  4sqlem1  13195  4sqlem2  13196  4sqlem4  13199  mul4sq  13201  4sqlem12  13209  4sqlem13m  13210  4sqlem18  13215  imasaddfnlemg  13693  imasmnd2  13817  imasgrp2  13971  imasrng  14361  imasring  14477  dvdsrtr  14516  isnzr2  14599  lss1d  14828  znidom  15100  restbasg  15411  txbas  15501  blin2  15675  xmettxlem  15752  xmettx  15753  addcncntoplem  15804  mulcncf  15851  plyf  15980  plyadd  15994  plymul  15995  plyco  16002  plycj  16004  plycn  16005  plyrecj  16006  dvply2g  16009  logbgcd1irr  16220  logbgcd1irrap  16223  zprmlogbap  16235  2sqlem5  16460  2sqlem9  16465  upgrpredgv  16609  usgredg4  16678  usgr1vr  16711  qdiff  17322