Theorem rexlimdvv 3037

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)

Hypothesis

Ref	Expression
rexlimdvv.1	|- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )

Assertion

Ref	Expression
rexlimdvv	|- ( 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 rexlimdvv

Step	Hyp	Ref	Expression
1		rexlimdvv.1	. . . 4 |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )
2	1	expdimp 453	. . 3 |- ( ( ph /\ x e. A ) -> ( y e. B -> ( ps -> ch ) ) )
3	2	rexlimdv 3030	. 2 |- ( ( ph /\ x e. A ) -> ( E. y e. B ps -> ch ) )
4	3	rexlimdva 3031	1 |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  rexlimdvva  3038  f1oiso2  6602  omeu  7665  xpdom2  8055  elfiun  8336  rankxplim3  8744  brdom6disj  9354  fpwwe2lem12  9463  tskxpss  9594  genpss  9826  genpcd  9828  genpnmax  9829  distrlem1pr  9847  distrlem5pr  9849  ltexprlem6  9863  reclem4pr  9872  supadd  10991  supmullem1  10993  supmullem2  10994  qaddcl  11804  qmulcl  11806  sqrlem6  13988  caubnd  14098  summo  14448  bezoutlem3  15258  bezoutlem4  15259  dvdsgcd  15261  gcddiv  15268  pceu  15551  pcqcl  15561  lspfixed  19128  lspexch  19129  lsmcv  19141  lspsolvlem  19142  hausnei2  21157  uncmp  21206  txcnp  21423  tx1stc  21453  fbasrn  21688  rnelfmlem  21756  blssps  22229  blss  22230  tgqioo  22603  ovolunlem2  23266  ax5seg  25818  axpasch  25821  axeuclid  25843  upgredg2vtx  26036  pjhthmo  28161  shmodsi  28248  pjpjpre  28278  chscllem4  28499  sumdmdlem  29277  cdj3lem2a  29295  cdj3lem2b  29296  cdj3lem3a  29298  dya2iocnrect  30343  fprb  31669  btwndiff  32134  btwnconn1lem13  32206  btwnconn1lem14  32207  brsegle  32215  segletr  32221  segleantisym  32222  nn0prpwlem  32317  ismblfin  33450  heibor1lem  33608  crngohomfo  33805  lsmsat  34295  3dim1  34753  3dim3  34755  1cvratex  34759  atcvrlln2  34805  atcvrlln  34806  lplnnlelln  34829  llncvrlpln2  34843  lplnexllnN  34850  2llnjN  34853  lvolnlelln  34870  lvolnlelpln  34871  lplncvrlvol2  34901  2lplnj  34906  lneq2at  35064  lnatexN  35065  lncvrat  35068  lncmp  35069  paddasslem15  35120  paddasslem16  35121  pmodlem2  35133  pmapjoin  35138  llnexchb2  35155  lhp2lt  35287  cdlemf  35851  cdlemg1cex  35876  cdlemg2ce  35880  cdlemn11pre  36499  dihord2pre  36514  dihord4  36547  dihmeetlem20N  36615  mapdpglem24  36993  mapdpglem32  36994  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  hdmapglem7  37221  mzpcompact2lem  37314  pellex  37399  disjrnmpt2  39375  mullimc  39848  mullimcf  39855  addlimc  39880  limclner  39883  fourierdlem42  40366  fourierdlem80  40403  fourierdlem97  40420  sge0resplit  40623  volicorescl  40767  opnvonmbllem2  40847  smfaddlem1  40971  smflimlem6  40984  gbepos  41646  gbowpos  41647  gbegt5  41649  gboge9  41652