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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  rexlimdvva  3219  fprb  7200  f1oiso2  7361  omeu  8597  xpdom2  9095  rex2dom  9248  elfiun  9426  rankxplim3  9902  brdom6disj  10615  fpwwe2lem11  10730  tskxpss  10861  genpss  11093  genpcd  11095  genpnmax  11096  distrlem1pr  11114  distrlem5pr  11116  ltexprlem6  11130  reclem4pr  11139  supadd  12289  supmullem1  12291  supmullem2  12292  qaddcl  13097  qmulcl  13099  01sqrexlem6  15420  caubnd  15532  summo  15889  bezoutlem3  16720  bezoutlem4  16721  dvdsgcd  16723  gcddiv  16730  pceu  17030  pcqcl  17040  symgpssefmnd  19616  crngrhmfo  20732  lspfixed  21412  lspexch  21413  lsmcv  21425  lspsolvlem  21426  hausnei2  23677  uncmp  23727  txcnp  23945  tx1stc  23975  fbasrn  24209  rnelfmlem  24277  blssps  24749  blss  24750  tgqioo  25125  ovolunlem2  25825  2sqnn  27772  madebdayim  28280  ax5seg  29522  axpasch  29525  axeuclid  29547  upgredg2vtx  29725  pjhthmo  31910  shmodsi  31997  pjpjpre  32027  chscllem4  32248  sumdmdlem  33026  cdj3lem2a  33044  cdj3lem2b  33045  cdj3lem3a  33047  dya2iocnrect  34960  satffunlem2lem1  36256  btwndiff  36885  btwnconn1lem13  36957  btwnconn1lem14  36958  brsegle  36966  segletr  36972  segleantisym  36973  nn0prpwlem  37203  ismblfin  38673  heibor1lem  38837  crngohomfo  39034  lsmsat  40159  3dim1  40618  3dim3  40620  1cvratex  40624  atcvrlln2  40670  atcvrlln  40671  lplnnlelln  40694  llncvrlpln2  40708  lplnexllnN  40715  2llnjN  40718  lvolnlelln  40735  lvolnlelpln  40736  lplncvrlvol2  40766  2lplnj  40771  lneq2at  40929  lnatexN  40930  lncvrat  40933  lncmp  40934  paddasslem15  40985  paddasslem16  40986  pmodlem2  40998  pmapjoin  41003  llnexchb2  41020  lhp2lt  41152  cdlemf  41714  cdlemg1cex  41739  cdlemg2ce  41743  cdlemn11pre  42361  dihord2pre  42376  dihord4  42409  dihmeetlem20N  42477  mapdpglem24  42855  mapdpglem32  42856  baerlem3lem2  42861  baerlem5alem2  42862  baerlem5blem2  42863  hdmapglem7  43080  sn-addlid  43549  rexlimdv3d  43787  mzpcompact2lem  43856  pellex  43936  onexomgt  44337  onexoegt  44340  oaun3lem1  44470  oaun3lem2  44471  disjrnmpt2  46297  mullimc  46722  mullimcf  46729  addlimc  46752  limclner  46755  fourierdlem42  47253  fourierdlem80  47290  fourierdlem97  47307  sge0resplit  47510  volicorescl  47657  opnvonmbllem2  47737  smfaddlem1  47867  smflimlem6  47880  gbepos  48950  gbowpos  48951  gbegt5  48953  gboge9  48956  isuspgrimlem  49087  usgrgrtrirex  49142  isubgr3stgrlem6  49163  gpgcubic  49271  gpg5nbgr3star  49273  pgnbgreunbgrlem3  49310  pgnbgreunbgrlem6  49316  pgnbgreunbgr  49317  seposep  50134  iscnrm3lem6  50146