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  7196  f1oiso2  7357  omeu  8576  xpdom2  9074  rex2dom  9227  elfiun  9404  rankxplim3  9867  brdom6disj  10539  fpwwe2lem11  10654  tskxpss  10785  genpss  11017  genpcd  11019  genpnmax  11020  distrlem1pr  11038  distrlem5pr  11040  ltexprlem6  11054  reclem4pr  11063  supadd  12211  supmullem1  12213  supmullem2  12214  qaddcl  13019  qmulcl  13021  01sqrexlem6  15338  caubnd  15450  summo  15807  bezoutlem3  16637  bezoutlem4  16638  dvdsgcd  16640  gcddiv  16647  pceu  16944  pcqcl  16954  symgpssefmnd  19529  crngrhmfo  20643  lspfixed  21321  lspexch  21322  lsmcv  21334  lspsolvlem  21335  hausnei2  23584  uncmp  23634  txcnp  23852  tx1stc  23882  fbasrn  24116  rnelfmlem  24184  blssps  24656  blss  24657  tgqioo  25032  ovolunlem2  25732  2sqnn  27683  madebdayim  28161  ax5seg  29403  axpasch  29406  axeuclid  29428  upgredg2vtx  29606  pjhthmo  31791  shmodsi  31878  pjpjpre  31908  chscllem4  32129  sumdmdlem  32907  cdj3lem2a  32925  cdj3lem2b  32926  cdj3lem3a  32928  dya2iocnrect  34800  satffunlem2lem1  35991  btwndiff  36615  btwnconn1lem13  36687  btwnconn1lem14  36688  brsegle  36696  segletr  36702  segleantisym  36703  nn0prpwlem  36949  ismblfin  38418  heibor1lem  38567  crngohomfo  38764  lsmsat  39889  3dim1  40348  3dim3  40350  1cvratex  40354  atcvrlln2  40400  atcvrlln  40401  lplnnlelln  40424  llncvrlpln2  40438  lplnexllnN  40445  2llnjN  40448  lvolnlelln  40465  lvolnlelpln  40466  lplncvrlvol2  40496  2lplnj  40501  lneq2at  40659  lnatexN  40660  lncvrat  40663  lncmp  40664  paddasslem15  40715  paddasslem16  40716  pmodlem2  40728  pmapjoin  40733  llnexchb2  40750  lhp2lt  40882  cdlemf  41444  cdlemg1cex  41469  cdlemg2ce  41473  cdlemn11pre  42091  dihord2pre  42106  dihord4  42139  dihmeetlem20N  42207  mapdpglem24  42585  mapdpglem32  42586  baerlem3lem2  42591  baerlem5alem2  42592  baerlem5blem2  42593  hdmapglem7  42810  sn-addlid  43287  rexlimdv3d  43536  mzpcompact2lem  43604  pellex  43684  onexomgt  44090  onexoegt  44093  oaun3lem1  44223  oaun3lem2  44224  disjrnmpt2  46028  mullimc  46454  mullimcf  46461  addlimc  46484  limclner  46487  fourierdlem42  46985  fourierdlem80  47022  fourierdlem97  47039  sge0resplit  47242  volicorescl  47389  opnvonmbllem2  47469  smfaddlem1  47599  smflimlem6  47612  gbepos  48682  gbowpos  48683  gbegt5  48685  gboge9  48688  isuspgrimlem  48819  usgrgrtrirex  48874  isubgr3stgrlem6  48895  gpgcubic  49003  gpg5nbgr3star  49005  pgnbgreunbgrlem3  49042  pgnbgreunbgrlem6  49048  pgnbgreunbgr  49049  seposep  49860  iscnrm3lem6  49872