Theorem rexlimdvv 3193

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexlimdvva  3194  fprb  7168  f1oiso2  7327  omeu  8549  xpdom2  9036  rex2dom  9193  elfiun  9381  rankxplim3  9834  brdom6disj  10485  fpwwe2lem11  10594  tskxpss  10725  genpss  10957  genpcd  10959  genpnmax  10960  distrlem1pr  10978  distrlem5pr  10980  ltexprlem6  10994  reclem4pr  11003  supadd  12151  supmullem1  12153  supmullem2  12154  qaddcl  12924  qmulcl  12926  01sqrexlem6  15213  caubnd  15325  summo  15683  bezoutlem3  16511  bezoutlem4  16512  dvdsgcd  16514  gcddiv  16521  pceu  16817  pcqcl  16827  symgpssefmnd  19326  lspfixed  21038  lspexch  21039  lsmcv  21051  lspsolvlem  21052  hausnei2  23240  uncmp  23290  txcnp  23507  tx1stc  23537  fbasrn  23771  rnelfmlem  23839  blssps  24312  blss  24313  tgqioo  24688  ovolunlem2  25399  2sqnn  27350  madebdayim  27799  ax5seg  28865  axpasch  28868  axeuclid  28890  upgredg2vtx  29068  pjhthmo  31231  shmodsi  31318  pjpjpre  31348  chscllem4  31569  sumdmdlem  32347  cdj3lem2a  32365  cdj3lem2b  32366  cdj3lem3a  32368  dya2iocnrect  34272  satffunlem2lem1  35391  btwndiff  36015  btwnconn1lem13  36087  btwnconn1lem14  36088  brsegle  36096  segletr  36102  segleantisym  36103  nn0prpwlem  36310  ismblfin  37655  heibor1lem  37803  crngohomfo  38000  lsmsat  39001  3dim1  39461  3dim3  39463  1cvratex  39467  atcvrlln2  39513  atcvrlln  39514  lplnnlelln  39537  llncvrlpln2  39551  lplnexllnN  39558  2llnjN  39561  lvolnlelln  39578  lvolnlelpln  39579  lplncvrlvol2  39609  2lplnj  39614  lneq2at  39772  lnatexN  39773  lncvrat  39776  lncmp  39777  paddasslem15  39828  paddasslem16  39829  pmodlem2  39841  pmapjoin  39846  llnexchb2  39863  lhp2lt  39995  cdlemf  40557  cdlemg1cex  40582  cdlemg2ce  40586  cdlemn11pre  41204  dihord2pre  41219  dihord4  41252  dihmeetlem20N  41320  mapdpglem24  41698  mapdpglem32  41699  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  hdmapglem7  41923  sn-addlid  42392  rexlimdv3d  42671  mzpcompact2lem  42739  pellex  42823  onexomgt  43230  onexoegt  43233  oaun3lem1  43363  oaun3lem2  43364  disjrnmpt2  45182  mullimc  45614  mullimcf  45621  addlimc  45646  limclner  45649  fourierdlem42  46147  fourierdlem80  46184  fourierdlem97  46201  sge0resplit  46404  volicorescl  46551  opnvonmbllem2  46631  smfaddlem1  46761  smflimlem6  46774  gbepos  47759  gbowpos  47760  gbegt5  47762  gboge9  47765  isuspgrimlem  47895  usgrgrtrirex  47949  isubgr3stgrlem6  47970  gpgcubic  48070  gpg5nbgr3star  48072  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  pgnbgreunbgr  48115  seposep  48914  iscnrm3lem6  48926