Theorem mptexd 7158

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 7155. (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 7155	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436   ↦ cmpt 5172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5217  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489

This theorem is referenced by:  mptsuppdifd  8116  mpocurryvald  8200  fsetfocdm  8785  fsuppssov1  9268  fsuppmptif  9283  sniffsupp  9284  cantnfrescl  9566  cantnflem1  9579  infxpenc2lem2  9911  ac5num  9927  ac6num  10370  negfi  12071  seqof2  13967  ramcl  16941  prdsplusgval  17377  prdsmulrval  17379  prdsvscaval  17383  galactghm  19317  gsum2dlem2  19884  gsum2d  19885  dprdfinv  19934  dprdfadd  19935  dmdprdsplitlem  19952  dpjfval  19970  dpjidcl  19973  mptscmfsupp0  20861  frlmgsum  21710  frlmphllem  21718  psrass1lem  21870  psrridm  21901  psrcom  21906  mvrfval  21919  mplcoe5  21976  mplbas2  21978  evlslem6  22017  selvffval  22049  psdffval  22073  psdfval  22074  psdmplcl  22078  psdmul  22082  evls1sca  22239  evls1fpws  22285  matgsum  22353  mvmulval  22459  mavmul0g  22469  marepvval0  22482  ptcnplem  23537  xkocnv  23730  ptcmplem3  23970  prdsdsf  24283  ressprdsds  24287  prdsxmslem2  24445  rrx0  25325  tdeglem4  25993  pserulm  26359  efsubm  26488  addsuniflem  27945  suppovss  32660  fisuppov1  32662  mptiffisupp  32672  fsuppcurry1  32705  fsuppcurry2  32706  gsummptres2  33031  gsumfs2d  33033  tocycval  33075  rmfsupp2  33203  elrgspnlem2  33208  elrsp  33335  qusrn  33372  elrspunidl  33391  elrspunsn  33392  mplvrpmfgalem  33572  mplvrpmga  33573  mplvrpmmhm  33574  mplvrpmrhm  33575  issply  33582  drgextgsum  33605  ply1degltdimlem  33633  fedgmullem2  33641  evls1fldgencl  33681  fldextrspunlsplem  33684  fldextrspunlsp  33685  extdgfialglem1  33703  extdgfialglem2  33704  minplyval  33716  ofcfval  34109  lpadval  34687  bj-imdirvallem  37220  hashscontpow  42161  aks6d1c2  42169  sticksstones4  42188  sticksstones11  42195  sticksstones12a  42196  sticksstones12  42197  sticksstones17  42202  sticksstones18  42203  sticksstones19  42204  sticksstones20  42205  aks6d1c6lem2  42210  aks6d1c6lem3  42211  aks6d1c7lem2  42220  aks5lem2  42226  evlsvvvallem  42600  evlsvvval  42602  selvvvval  42624  evlselv  42626  mhphf  42636  rfovfvd  44041  fsovfvd  44049  dssmapf1od  44060  choicefi  45243  axccdom  45265  climeldmeqmpt  45712  climfveqmpt  45715  climfveqmpt3  45726  climeldmeqmpt3  45733  climfveqmpt2  45737  climeldmeqmpt2  45739  climeqmpt  45741  limsupresicompt  45800  liminfresicompt  45824  liminfvalxr  45827  liminflbuz2  45859  iccvonmbllem  46722  vonioolem1  46724  vonioolem2  46725  vonicclem1  46727  vonicclem2  46728  smflimmpt  46854  smflimsuplem6  46869  cfsetsnfsetfv  47094  cfsetsnfsetf  47095  fundcmpsurbijinjpreimafv  47444  prproropen  47545  isubgr3stgr  48012  uspgrbispr  48188  1arymaptfv  48678  1arymaptfo  48681  fuco22  49377