Theorem rexlimdvv 3218

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

Hypothesis

Ref	Expression
rexlimdvv.1	⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))

Assertion

Ref	Expression
rexlimdvv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Distinct variable groups:   𝑥,𝑦,𝜑   𝜒,𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimdvv

Step	Hyp	Ref	Expression
1		rexlimdvv.1	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
2	1	expdimp 452	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝜓 → 𝜒)))
3	2	rexlimdv 3159	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
4	3	rexlimdva 3161	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexlimdvva  3219  fprb  7231  f1oiso2  7388  omeu  8641  xpdom2  9133  rex2dom  9309  elfiun  9499  rankxplim3  9950  brdom6disj  10601  fpwwe2lem11  10710  tskxpss  10841  genpss  11073  genpcd  11075  genpnmax  11076  distrlem1pr  11094  distrlem5pr  11096  ltexprlem6  11110  reclem4pr  11119  supadd  12263  supmullem1  12265  supmullem2  12266  qaddcl  13030  qmulcl  13032  01sqrexlem6  15296  caubnd  15407  summo  15765  bezoutlem3  16588  bezoutlem4  16589  dvdsgcd  16591  gcddiv  16598  pceu  16893  pcqcl  16903  symgpssefmnd  19437  lspfixed  21153  lspexch  21154  lsmcv  21166  lspsolvlem  21167  hausnei2  23382  uncmp  23432  txcnp  23649  tx1stc  23679  fbasrn  23913  rnelfmlem  23981  blssps  24455  blss  24456  tgqioo  24841  ovolunlem2  25552  2sqnn  27501  madebdayim  27944  ax5seg  28971  axpasch  28974  axeuclid  28996  upgredg2vtx  29176  pjhthmo  31334  shmodsi  31421  pjpjpre  31451  chscllem4  31672  sumdmdlem  32450  cdj3lem2a  32468  cdj3lem2b  32469  cdj3lem3a  32471  dya2iocnrect  34246  satffunlem2lem1  35372  btwndiff  35991  btwnconn1lem13  36063  btwnconn1lem14  36064  brsegle  36072  segletr  36078  segleantisym  36079  nn0prpwlem  36288  ismblfin  37621  heibor1lem  37769  crngohomfo  37966  lsmsat  38964  3dim1  39424  3dim3  39426  1cvratex  39430  atcvrlln2  39476  atcvrlln  39477  lplnnlelln  39500  llncvrlpln2  39514  lplnexllnN  39521  2llnjN  39524  lvolnlelln  39541  lvolnlelpln  39542  lplncvrlvol2  39572  2lplnj  39577  lneq2at  39735  lnatexN  39736  lncvrat  39739  lncmp  39740  paddasslem15  39791  paddasslem16  39792  pmodlem2  39804  pmapjoin  39809  llnexchb2  39826  lhp2lt  39958  cdlemf  40520  cdlemg1cex  40545  cdlemg2ce  40549  cdlemn11pre  41167  dihord2pre  41182  dihord4  41215  dihmeetlem20N  41283  mapdpglem24  41661  mapdpglem32  41662  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  hdmapglem7  41886  sn-addlid  42380  rexlimdv3d  42639  mzpcompact2lem  42707  pellex  42791  onexomgt  43202  onexoegt  43205  oaun3lem1  43336  oaun3lem2  43337  disjrnmpt2  45095  mullimc  45537  mullimcf  45544  addlimc  45569  limclner  45572  fourierdlem42  46070  fourierdlem80  46107  fourierdlem97  46124  sge0resplit  46327  volicorescl  46474  opnvonmbllem2  46554  smfaddlem1  46684  smflimlem6  46697  gbepos  47632  gbowpos  47633  gbegt5  47635  gboge9  47638  isuspgrimlem  47758  usgrgrtrirex  47799  seposep  48605  iscnrm3lem6  48618