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  7182  f1oiso2  7336  omeu  8573  xpdom2  9055  rex2dom  9234  elfiun  9412  rankxplim3  9863  brdom6disj  10514  fpwwe2lem11  10623  tskxpss  10754  genpss  10986  genpcd  10988  genpnmax  10989  distrlem1pr  11007  distrlem5pr  11009  ltexprlem6  11023  reclem4pr  11032  supadd  12169  supmullem1  12171  supmullem2  12172  qaddcl  12936  qmulcl  12938  01sqrexlem6  15181  caubnd  15292  summo  15650  bezoutlem3  16470  bezoutlem4  16471  dvdsgcd  16473  gcddiv  16480  pceu  16766  pcqcl  16776  symgpssefmnd  19247  lspfixed  20718  lspexch  20719  lsmcv  20731  lspsolvlem  20732  hausnei2  22826  uncmp  22876  txcnp  23093  tx1stc  23123  fbasrn  23357  rnelfmlem  23425  blssps  23899  blss  23900  tgqioo  24285  ovolunlem2  24984  2sqnn  26909  madebdayim  27349  ax5seg  28163  axpasch  28166  axeuclid  28188  upgredg2vtx  28368  pjhthmo  30520  shmodsi  30607  pjpjpre  30637  chscllem4  30858  sumdmdlem  31636  cdj3lem2a  31654  cdj3lem2b  31655  cdj3lem3a  31657  dya2iocnrect  33211  satffunlem2lem1  34326  btwndiff  34930  btwnconn1lem13  35002  btwnconn1lem14  35003  brsegle  35011  segletr  35017  segleantisym  35018  nn0prpwlem  35112  ismblfin  36434  heibor1lem  36583  crngohomfo  36780  lsmsat  37784  3dim1  38244  3dim3  38246  1cvratex  38250  atcvrlln2  38296  atcvrlln  38297  lplnnlelln  38320  llncvrlpln2  38334  lplnexllnN  38341  2llnjN  38344  lvolnlelln  38361  lvolnlelpln  38362  lplncvrlvol2  38392  2lplnj  38397  lneq2at  38555  lnatexN  38556  lncvrat  38559  lncmp  38560  paddasslem15  38611  paddasslem16  38612  pmodlem2  38624  pmapjoin  38629  llnexchb2  38646  lhp2lt  38778  cdlemf  39340  cdlemg1cex  39365  cdlemg2ce  39369  cdlemn11pre  39987  dihord2pre  40002  dihord4  40035  dihmeetlem20N  40103  mapdpglem24  40481  mapdpglem32  40482  baerlem3lem2  40487  baerlem5alem2  40488  baerlem5blem2  40489  hdmapglem7  40706  sn-addlid  41159  rexlimdv3d  41292  mzpcompact2lem  41360  pellex  41444  onexomgt  41861  onexoegt  41864  oaun3lem1  41995  oaun3lem2  41996  disjrnmpt2  43757  mullimc  44205  mullimcf  44212  addlimc  44237  limclner  44240  fourierdlem42  44738  fourierdlem80  44775  fourierdlem97  44792  sge0resplit  44995  volicorescl  45142  opnvonmbllem2  45222  smfaddlem1  45352  smflimlem6  45365  gbepos  46299  gbowpos  46300  gbegt5  46302  gboge9  46305  seposep  47398  iscnrm3lem6  47411