Theorem rexlimdvv 3224

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

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

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 3093

This theorem is used by:  rexlimdvva  3225  fprb  7199  f1oiso2  7361  omeu  8579  xpdom2  9070  rex2dom  9223  elfiun  9400  rankxplim3  9863  brdom6disj  10534  fpwwe2lem11  10644  tskxpss  10775  genpss  11007  genpcd  11009  genpnmax  11010  distrlem1pr  11028  distrlem5pr  11030  ltexprlem6  11044  reclem4pr  11053  supadd  12201  supmullem1  12203  supmullem2  12204  qaddcl  13007  qmulcl  13009  01sqrexlem6  15324  caubnd  15436  summo  15794  bezoutlem3  16624  bezoutlem4  16625  dvdsgcd  16627  gcddiv  16634  pceu  16931  pcqcl  16941  symgpssefmnd  19497  crngrhmfo  20611  lspfixed  21289  lspexch  21290  lsmcv  21302  lspsolvlem  21303  hausnei2  23547  uncmp  23597  txcnp  23814  tx1stc  23844  fbasrn  24078  rnelfmlem  24146  blssps  24618  blss  24619  tgqioo  24994  ovolunlem2  25694  2sqnn  27640  madebdayim  28118  ax5seg  29325  axpasch  29328  axeuclid  29350  upgredg2vtx  29528  pjhthmo  31691  shmodsi  31778  pjpjpre  31808  chscllem4  32029  sumdmdlem  32807  cdj3lem2a  32825  cdj3lem2b  32826  cdj3lem3a  32828  dya2iocnrect  34703  satffunlem2lem1  35917  btwndiff  36540  btwnconn1lem13  36612  btwnconn1lem14  36613  brsegle  36621  segletr  36627  segleantisym  36628  nn0prpwlem  36874  ismblfin  38353  heibor1lem  38501  crngohomfo  38698  lsmsat  39823  3dim1  40282  3dim3  40284  1cvratex  40288  atcvrlln2  40334  atcvrlln  40335  lplnnlelln  40358  llncvrlpln2  40372  lplnexllnN  40379  2llnjN  40382  lvolnlelln  40399  lvolnlelpln  40400  lplncvrlvol2  40430  2lplnj  40435  lneq2at  40593  lnatexN  40594  lncvrat  40597  lncmp  40598  paddasslem15  40649  paddasslem16  40650  pmodlem2  40662  pmapjoin  40667  llnexchb2  40684  lhp2lt  40816  cdlemf  41378  cdlemg1cex  41403  cdlemg2ce  41407  cdlemn11pre  42025  dihord2pre  42040  dihord4  42073  dihmeetlem20N  42141  mapdpglem24  42519  mapdpglem32  42520  baerlem3lem2  42525  baerlem5alem2  42526  baerlem5blem2  42527  hdmapglem7  42744  sn-addlid  43206  rexlimdv3d  43455  mzpcompact2lem  43523  pellex  43603  onexomgt  44009  onexoegt  44012  oaun3lem1  44142  oaun3lem2  44143  disjrnmpt2  45947  mullimc  46373  mullimcf  46380  addlimc  46403  limclner  46406  fourierdlem42  46904  fourierdlem80  46941  fourierdlem97  46958  sge0resplit  47161  volicorescl  47308  opnvonmbllem2  47388  smfaddlem1  47518  smflimlem6  47531  gbepos  48564  gbowpos  48565  gbegt5  48567  gboge9  48570  isuspgrimlem  48701  usgrgrtrirex  48756  isubgr3stgrlem6  48777  gpgcubic  48885  gpg5nbgr3star  48887  pgnbgreunbgrlem3  48924  pgnbgreunbgrlem6  48930  pgnbgreunbgr  48931  seposep  49745  iscnrm3lem6  49757