Theorem mptexd 7172

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 7169. (Contributed by Glauco Siliprandi, 24-Dec-2020.)

Hypothesis

Ref	Expression
mptexd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
mptexd	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem mptexd

Step	Hyp	Ref	Expression
1		mptexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		mptexg 7169	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   ↦ cmpt 5167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500

This theorem is referenced by:  mptsuppdifd  8129  mpocurryvald  8213  fsetfocdm  8801  fsuppssov1  9290  fsuppmptif  9305  sniffsupp  9306  cantnfrescl  9588  cantnflem1  9601  infxpenc2lem2  9933  ac5num  9949  ac6num  10392  negfi  12096  seqof2  14013  ramcl  16991  prdsplusgval  17427  prdsmulrval  17429  prdsvscaval  17433  galactghm  19370  gsum2dlem2  19937  gsum2d  19938  dprdfinv  19987  dprdfadd  19988  dmdprdsplitlem  20005  dpjfval  20023  dpjidcl  20026  mptscmfsupp0  20913  frlmgsum  21762  frlmphllem  21770  psrass1lem  21922  psrridm  21951  psrcom  21956  mvrfval  21969  mplcoe5  22028  mplbas2  22030  evlslem6  22069  evlsvvvallem  22079  evlsvvval  22081  selvffval  22109  psdffval  22133  psdfval  22134  psdmplcl  22138  psdmul  22142  evls1sca  22298  evls1fpws  22344  matgsum  22412  mvmulval  22518  mavmul0g  22528  marepvval0  22541  ptcnplem  23596  xkocnv  23789  ptcmplem3  24029  prdsdsf  24342  ressprdsds  24346  prdsxmslem2  24504  rrx0  25374  tdeglem4  26035  pserulm  26400  efsubm  26528  addsuniflem  28007  suppovss  32769  fisuppov1  32771  mptiffisupp  32781  fsuppcurry1  32812  fsuppcurry2  32813  gsummptres2  33129  gsumfs2d  33137  tocycval  33184  rmfsupp2  33314  elrgspnlem2  33319  elrsp  33447  qusrn  33484  elrspunidl  33503  elrspunsn  33504  extvval  33690  extvfv  33692  extvfvcl  33695  extvfvalf  33696  mplvrpmfgalem  33703  mplvrpmga  33704  mplvrpmmhm  33705  mplvrpmrhm  33706  psrmonmul2  33710  issply  33720  esplyfvaln  33733  drgextgsum  33754  ply1degltdimlem  33782  fedgmullem2  33790  evls1fldgencl  33830  fldextrspunlsplem  33833  fldextrspunlsp  33834  extdgfialglem1  33852  extdgfialglem2  33853  minplyval  33865  ofcfval  34258  lpadval  34836  bj-imdirvallem  37510  qmapex  38786  hashscontpow  42575  aks6d1c2  42583  sticksstones4  42602  sticksstones11  42609  sticksstones12a  42610  sticksstones12  42611  sticksstones17  42616  sticksstones18  42617  sticksstones19  42618  sticksstones20  42619  aks6d1c6lem2  42624  aks6d1c6lem3  42625  aks6d1c7lem2  42634  aks5lem2  42640  selvvvval  43032  evlselv  43034  mhphf  43044  rfovfvd  44447  fsovfvd  44455  dssmapf1od  44466  choicefi  45647  axccdom  45669  climeldmeqmpt  46114  climfveqmpt  46117  climfveqmpt3  46128  climeldmeqmpt3  46135  climfveqmpt2  46139  climeldmeqmpt2  46141  climeqmpt  46143  limsupresicompt  46202  liminfresicompt  46226  liminfvalxr  46229  liminflbuz2  46261  iccvonmbllem  47124  vonioolem1  47126  vonioolem2  47127  vonicclem1  47129  vonicclem2  47130  smflimmpt  47256  smflimsuplem6  47271  cfsetsnfsetfv  47517  cfsetsnfsetf  47518  fundcmpsurbijinjpreimafv  47879  prproropen  47980  isubgr3stgr  48463  uspgrbispr  48639  1arymaptfv  49128  1arymaptfo  49131  fuco22  49826