Theorem rexlimdvv 3211

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rexlimdvva  3212  fprb  7192  f1oiso2  7346  omeu  8582  xpdom2  9064  rex2dom  9243  elfiun  9422  rankxplim3  9873  brdom6disj  10524  fpwwe2lem11  10633  tskxpss  10764  genpss  10996  genpcd  10998  genpnmax  10999  distrlem1pr  11017  distrlem5pr  11019  ltexprlem6  11033  reclem4pr  11042  supadd  12179  supmullem1  12181  supmullem2  12182  qaddcl  12946  qmulcl  12948  01sqrexlem6  15191  caubnd  15302  summo  15660  bezoutlem3  16480  bezoutlem4  16481  dvdsgcd  16483  gcddiv  16490  pceu  16776  pcqcl  16786  symgpssefmnd  19258  lspfixed  20734  lspexch  20735  lsmcv  20747  lspsolvlem  20748  hausnei2  22849  uncmp  22899  txcnp  23116  tx1stc  23146  fbasrn  23380  rnelfmlem  23448  blssps  23922  blss  23923  tgqioo  24308  ovolunlem2  25007  2sqnn  26932  madebdayim  27372  ax5seg  28186  axpasch  28189  axeuclid  28211  upgredg2vtx  28391  pjhthmo  30543  shmodsi  30630  pjpjpre  30660  chscllem4  30881  sumdmdlem  31659  cdj3lem2a  31677  cdj3lem2b  31678  cdj3lem3a  31680  dya2iocnrect  33269  satffunlem2lem1  34384  btwndiff  34988  btwnconn1lem13  35060  btwnconn1lem14  35061  brsegle  35069  segletr  35075  segleantisym  35076  nn0prpwlem  35196  ismblfin  36518  heibor1lem  36666  crngohomfo  36863  lsmsat  37867  3dim1  38327  3dim3  38329  1cvratex  38333  atcvrlln2  38379  atcvrlln  38380  lplnnlelln  38403  llncvrlpln2  38417  lplnexllnN  38424  2llnjN  38427  lvolnlelln  38444  lvolnlelpln  38445  lplncvrlvol2  38475  2lplnj  38480  lneq2at  38638  lnatexN  38639  lncvrat  38642  lncmp  38643  paddasslem15  38694  paddasslem16  38695  pmodlem2  38707  pmapjoin  38712  llnexchb2  38729  lhp2lt  38861  cdlemf  39423  cdlemg1cex  39448  cdlemg2ce  39452  cdlemn11pre  40070  dihord2pre  40085  dihord4  40118  dihmeetlem20N  40186  mapdpglem24  40564  mapdpglem32  40565  baerlem3lem2  40570  baerlem5alem2  40571  baerlem5blem2  40572  hdmapglem7  40789  sn-addlid  41274  rexlimdv3d  41407  mzpcompact2lem  41475  pellex  41559  onexomgt  41976  onexoegt  41979  oaun3lem1  42110  oaun3lem2  42111  disjrnmpt2  43872  mullimc  44319  mullimcf  44326  addlimc  44351  limclner  44354  fourierdlem42  44852  fourierdlem80  44889  fourierdlem97  44906  sge0resplit  45109  volicorescl  45256  opnvonmbllem2  45336  smfaddlem1  45466  smflimlem6  45479  gbepos  46413  gbowpos  46414  gbegt5  46416  gboge9  46419  seposep  47512  iscnrm3lem6  47525