Theorem rexlimdvv 3220

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 458	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝜓 → 𝜒)))
3	2	rexlimdv 3163	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
4	3	rexlimdva 3165	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3089

This theorem is used by:  rexlimdvva  3221  fprb  7195  f1oiso2  7356  omeu  8575  xpdom2  9073  rex2dom  9226  elfiun  9403  rankxplim3  9866  brdom6disj  10538  fpwwe2lem11  10653  tskxpss  10784  genpss  11016  genpcd  11018  genpnmax  11019  distrlem1pr  11037  distrlem5pr  11039  ltexprlem6  11053  reclem4pr  11062  supadd  12210  supmullem1  12212  supmullem2  12213  qaddcl  13017  qmulcl  13019  01sqrexlem6  15336  caubnd  15448  summo  15805  bezoutlem3  16635  bezoutlem4  16636  dvdsgcd  16638  gcddiv  16645  pceu  16942  pcqcl  16952  symgpssefmnd  19524  crngrhmfo  20638  lspfixed  21316  lspexch  21317  lsmcv  21329  lspsolvlem  21330  hausnei2  23579  uncmp  23629  txcnp  23847  tx1stc  23877  fbasrn  24111  rnelfmlem  24179  blssps  24651  blss  24652  tgqioo  25027  ovolunlem2  25727  2sqnn  27673  madebdayim  28151  ax5seg  29381  axpasch  29384  axeuclid  29406  upgredg2vtx  29584  pjhthmo  31769  shmodsi  31856  pjpjpre  31886  chscllem4  32107  sumdmdlem  32885  cdj3lem2a  32903  cdj3lem2b  32904  cdj3lem3a  32906  dya2iocnrect  34779  satffunlem2lem1  35970  btwndiff  36594  btwnconn1lem13  36666  btwnconn1lem14  36667  brsegle  36675  segletr  36681  segleantisym  36682  nn0prpwlem  36928  ismblfin  38397  heibor1lem  38546  crngohomfo  38743  lsmsat  39868  3dim1  40327  3dim3  40329  1cvratex  40333  atcvrlln2  40379  atcvrlln  40380  lplnnlelln  40403  llncvrlpln2  40417  lplnexllnN  40424  2llnjN  40427  lvolnlelln  40444  lvolnlelpln  40445  lplncvrlvol2  40475  2lplnj  40480  lneq2at  40638  lnatexN  40639  lncvrat  40642  lncmp  40643  paddasslem15  40694  paddasslem16  40695  pmodlem2  40707  pmapjoin  40712  llnexchb2  40729  lhp2lt  40861  cdlemf  41423  cdlemg1cex  41448  cdlemg2ce  41452  cdlemn11pre  42070  dihord2pre  42085  dihord4  42118  dihmeetlem20N  42186  mapdpglem24  42564  mapdpglem32  42565  baerlem3lem2  42570  baerlem5alem2  42571  baerlem5blem2  42572  hdmapglem7  42789  sn-addlid  43266  rexlimdv3d  43515  mzpcompact2lem  43583  pellex  43663  onexomgt  44069  onexoegt  44072  oaun3lem1  44202  oaun3lem2  44203  disjrnmpt2  46007  mullimc  46433  mullimcf  46440  addlimc  46463  limclner  46466  fourierdlem42  46964  fourierdlem80  47001  fourierdlem97  47018  sge0resplit  47221  volicorescl  47368  opnvonmbllem2  47448  smfaddlem1  47578  smflimlem6  47591  gbepos  48661  gbowpos  48662  gbegt5  48664  gboge9  48667  isuspgrimlem  48798  usgrgrtrirex  48853  isubgr3stgrlem6  48874  gpgcubic  48982  gpg5nbgr3star  48984  pgnbgreunbgrlem3  49021  pgnbgreunbgrlem6  49027  pgnbgreunbgr  49028  seposep  49839  iscnrm3lem6  49851