Theorem rexlimdvv 3221

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  rexlimdvva  3222  fprb  7182  f1oiso2  7340  omeu  8558  xpdom2  9048  rex2dom  9201  elfiun  9378  rankxplim3  9841  brdom6disj  10504  fpwwe2lem11  10614  tskxpss  10745  genpss  10977  genpcd  10979  genpnmax  10980  distrlem1pr  10998  distrlem5pr  11000  ltexprlem6  11014  reclem4pr  11023  supadd  12174  supmullem1  12176  supmullem2  12177  qaddcl  12980  qmulcl  12982  01sqrexlem6  15288  caubnd  15400  summo  15758  bezoutlem3  16589  bezoutlem4  16590  dvdsgcd  16592  gcddiv  16599  pceu  16896  pcqcl  16906  symgpssefmnd  19457  lspfixed  21221  lspexch  21222  lsmcv  21234  lspsolvlem  21235  hausnei2  23471  uncmp  23521  txcnp  23738  tx1stc  23768  fbasrn  24002  rnelfmlem  24070  blssps  24542  blss  24543  tgqioo  24918  ovolunlem2  25618  2sqnn  27561  madebdayim  28039  ax5seg  29197  axpasch  29200  axeuclid  29222  upgredg2vtx  29400  pjhthmo  31563  shmodsi  31650  pjpjpre  31680  chscllem4  31901  sumdmdlem  32679  cdj3lem2a  32697  cdj3lem2b  32698  cdj3lem3a  32700  dya2iocnrect  34588  satffunlem2lem1  35767  btwndiff  36390  btwnconn1lem13  36462  btwnconn1lem14  36463  brsegle  36471  segletr  36477  segleantisym  36478  nn0prpwlem  36695  ismblfin  38172  heibor1lem  38320  crngohomfo  38517  lsmsat  39644  3dim1  40103  3dim3  40105  1cvratex  40109  atcvrlln2  40155  atcvrlln  40156  lplnnlelln  40179  llncvrlpln2  40193  lplnexllnN  40200  2llnjN  40203  lvolnlelln  40220  lvolnlelpln  40221  lplncvrlvol2  40251  2lplnj  40256  lneq2at  40414  lnatexN  40415  lncvrat  40418  lncmp  40419  paddasslem15  40470  paddasslem16  40471  pmodlem2  40483  pmapjoin  40488  llnexchb2  40505  lhp2lt  40637  cdlemf  41199  cdlemg1cex  41224  cdlemg2ce  41228  cdlemn11pre  41846  dihord2pre  41861  dihord4  41894  dihmeetlem20N  41962  mapdpglem24  42340  mapdpglem32  42341  baerlem3lem2  42346  baerlem5alem2  42347  baerlem5blem2  42348  hdmapglem7  42565  sn-addlid  43025  rexlimdv3d  43276  mzpcompact2lem  43344  pellex  43424  onexomgt  43830  onexoegt  43833  oaun3lem1  43963  oaun3lem2  43964  disjrnmpt2  45764  mullimc  46190  mullimcf  46197  addlimc  46220  limclner  46223  fourierdlem42  46721  fourierdlem80  46758  fourierdlem97  46775  sge0resplit  46978  volicorescl  47125  opnvonmbllem2  47205  smfaddlem1  47335  smflimlem6  47348  gbepos  48378  gbowpos  48379  gbegt5  48381  gboge9  48384  isuspgrimlem  48515  usgrgrtrirex  48570  isubgr3stgrlem6  48591  gpgcubic  48699  gpg5nbgr3star  48701  pgnbgreunbgrlem3  48738  pgnbgreunbgrlem6  48744  pgnbgreunbgr  48745  seposep  49555  iscnrm3lem6  49567