Theorem mptexd 7170

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440   ↦ cmpt 5179

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  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  8128  mpocurryvald  8212  fsetfocdm  8798  fsuppssov1  9287  fsuppmptif  9302  sniffsupp  9303  cantnfrescl  9585  cantnflem1  9598  infxpenc2lem2  9930  ac5num  9946  ac6num  10389  negfi  12091  seqof2  13983  ramcl  16957  prdsplusgval  17393  prdsmulrval  17395  prdsvscaval  17399  galactghm  19333  gsum2dlem2  19900  gsum2d  19901  dprdfinv  19950  dprdfadd  19951  dmdprdsplitlem  19968  dpjfval  19986  dpjidcl  19989  mptscmfsupp0  20878  frlmgsum  21727  frlmphllem  21735  psrass1lem  21888  psrridm  21918  psrcom  21923  mvrfval  21936  mplcoe5  21995  mplbas2  21997  evlslem6  22036  evlsvvvallem  22046  evlsvvval  22048  selvffval  22076  psdffval  22100  psdfval  22101  psdmplcl  22105  psdmul  22109  evls1sca  22267  evls1fpws  22313  matgsum  22381  mvmulval  22487  mavmul0g  22497  marepvval0  22510  ptcnplem  23565  xkocnv  23758  ptcmplem3  23998  prdsdsf  24311  ressprdsds  24315  prdsxmslem2  24473  rrx0  25353  tdeglem4  26021  pserulm  26387  efsubm  26516  addsuniflem  27997  suppovss  32760  fisuppov1  32762  mptiffisupp  32772  fsuppcurry1  32803  fsuppcurry2  32804  gsummptres2  33136  gsumfs2d  33144  tocycval  33190  rmfsupp2  33320  elrgspnlem2  33325  elrsp  33453  qusrn  33490  elrspunidl  33509  elrspunsn  33510  extvval  33696  extvfv  33698  extvfvcl  33701  extvfvalf  33702  mplvrpmfgalem  33709  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  issply  33719  drgextgsum  33751  ply1degltdimlem  33779  fedgmullem2  33787  evls1fldgencl  33827  fldextrspunlsplem  33830  fldextrspunlsp  33831  extdgfialglem1  33849  extdgfialglem2  33850  minplyval  33862  ofcfval  34255  lpadval  34833  bj-imdirvallem  37385  hashscontpow  42376  aks6d1c2  42384  sticksstones4  42403  sticksstones11  42410  sticksstones12a  42411  sticksstones12  42412  sticksstones17  42417  sticksstones18  42418  sticksstones19  42419  sticksstones20  42420  aks6d1c6lem2  42425  aks6d1c6lem3  42426  aks6d1c7lem2  42435  aks5lem2  42441  selvvvval  42828  evlselv  42830  mhphf  42840  rfovfvd  44243  fsovfvd  44251  dssmapf1od  44262  choicefi  45444  axccdom  45466  climeldmeqmpt  45912  climfveqmpt  45915  climfveqmpt3  45926  climeldmeqmpt3  45933  climfveqmpt2  45937  climeldmeqmpt2  45939  climeqmpt  45941  limsupresicompt  46000  liminfresicompt  46024  liminfvalxr  46027  liminflbuz2  46059  iccvonmbllem  46922  vonioolem1  46924  vonioolem2  46925  vonicclem1  46927  vonicclem2  46928  smflimmpt  47054  smflimsuplem6  47069  cfsetsnfsetfv  47303  cfsetsnfsetf  47304  fundcmpsurbijinjpreimafv  47653  prproropen  47754  isubgr3stgr  48221  uspgrbispr  48397  1arymaptfv  48886  1arymaptfo  48889  fuco22  49584