Theorem mptexd 7180

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   ↦ cmpt 5181

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 5226  ax-sep 5243  ax-nul 5253  ax-pr 5379

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 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508

This theorem is referenced by:  mptsuppdifd  8138  mpocurryvald  8222  fsetfocdm  8810  fsuppssov1  9299  fsuppmptif  9314  sniffsupp  9315  cantnfrescl  9597  cantnflem1  9610  infxpenc2lem2  9942  ac5num  9958  ac6num  10401  negfi  12103  seqof2  13995  ramcl  16969  prdsplusgval  17405  prdsmulrval  17407  prdsvscaval  17411  galactghm  19345  gsum2dlem2  19912  gsum2d  19913  dprdfinv  19962  dprdfadd  19963  dmdprdsplitlem  19980  dpjfval  19998  dpjidcl  20001  mptscmfsupp0  20890  frlmgsum  21739  frlmphllem  21747  psrass1lem  21900  psrridm  21930  psrcom  21935  mvrfval  21948  mplcoe5  22007  mplbas2  22009  evlslem6  22048  evlsvvvallem  22058  evlsvvval  22060  selvffval  22088  psdffval  22112  psdfval  22113  psdmplcl  22117  psdmul  22121  evls1sca  22279  evls1fpws  22325  matgsum  22393  mvmulval  22499  mavmul0g  22509  marepvval0  22522  ptcnplem  23577  xkocnv  23770  ptcmplem3  24010  prdsdsf  24323  ressprdsds  24327  prdsxmslem2  24485  rrx0  25365  tdeglem4  26033  pserulm  26399  efsubm  26528  addsuniflem  28009  suppovss  32770  fisuppov1  32772  mptiffisupp  32782  fsuppcurry1  32813  fsuppcurry2  32814  gsummptres2  33146  gsumfs2d  33154  tocycval  33201  rmfsupp2  33331  elrgspnlem2  33336  elrsp  33464  qusrn  33501  elrspunidl  33520  elrspunsn  33521  extvval  33707  extvfv  33709  extvfvcl  33712  extvfvalf  33713  mplvrpmfgalem  33720  mplvrpmga  33721  mplvrpmmhm  33722  mplvrpmrhm  33723  psrmonmul2  33727  issply  33737  esplyfvaln  33750  drgextgsum  33771  ply1degltdimlem  33799  fedgmullem2  33807  evls1fldgencl  33847  fldextrspunlsplem  33850  fldextrspunlsp  33851  extdgfialglem1  33869  extdgfialglem2  33870  minplyval  33882  ofcfval  34275  lpadval  34853  bj-imdirvallem  37432  qmapex  38699  hashscontpow  42489  aks6d1c2  42497  sticksstones4  42516  sticksstones11  42523  sticksstones12a  42524  sticksstones12  42525  sticksstones17  42530  sticksstones18  42531  sticksstones19  42532  sticksstones20  42533  aks6d1c6lem2  42538  aks6d1c6lem3  42539  aks6d1c7lem2  42548  aks5lem2  42554  selvvvval  42940  evlselv  42942  mhphf  42952  rfovfvd  44355  fsovfvd  44363  dssmapf1od  44374  choicefi  45555  axccdom  45577  climeldmeqmpt  46023  climfveqmpt  46026  climfveqmpt3  46037  climeldmeqmpt3  46044  climfveqmpt2  46048  climeldmeqmpt2  46050  climeqmpt  46052  limsupresicompt  46111  liminfresicompt  46135  liminfvalxr  46138  liminflbuz2  46170  iccvonmbllem  47033  vonioolem1  47035  vonioolem2  47036  vonicclem1  47038  vonicclem2  47039  smflimmpt  47165  smflimsuplem6  47180  cfsetsnfsetfv  47414  cfsetsnfsetf  47415  fundcmpsurbijinjpreimafv  47764  prproropen  47865  isubgr3stgr  48332  uspgrbispr  48508  1arymaptfv  48997  1arymaptfo  49000  fuco22  49695