Theorem mptexd 7261

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454   ↦ cmpt 5192

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574

This theorem is used by:  mptsuppdifd  8241  mpocurryvald  8325  fsetfocdm  8921  fsuppssov1  9413  fsuppmptif  9428  sniffsupp  9429  cantnfrescl  9714  cantnflem1  9727  infxpenc2lem2  10138  ac5num  10154  ac6num  10596  negfi  12306  seqof2  14243  ramcl  17251  prdsplusgval  17694  prdsmulrval  17696  prdsvscaval  17700  galactghm  19669  gsum2dlem2  20236  gsum2d  20237  dprdfinv  20286  dprdfadd  20287  dmdprdsplitlem  20304  dpjfval  20322  dpjidcl  20325  mptscmfsupp0  21253  frlmgsum  22133  frlmphllem  22141  psrass1lem  22296  psrridm  22325  psrcom  22330  mvrfval  22343  mplcoe5  22404  mplbas2  22406  evlslem6  22445  evlsvvvallem  22455  evlsvvval  22457  selvffval  22482  selvvvval  22506  psdffval  22533  psdfval  22534  psdmplcl  22538  psdmul  22542  evls1sca  22696  evls1fpws  22742  matgsum  22807  mvmulval  22913  mavmul0g  22923  marepvval0  22936  ptcnplem  23995  xkocnv  24188  ptcmplem3  24428  prdsdsf  24741  ressprdsds  24745  prdsxmslem2  24903  rrx0  25773  tdeglem4  26433  pserulm  26806  efsubm  26936  addsuniflem  28444  suppovss  33371  fisuppov1  33373  mptiffisupp  33383  fsuppcurry1  33412  fsuppcurry2  33413  gsummptres2  33713  gsumfs2d  33721  tocycval  33768  rmfsupp2  33897  elrgspnlem2  33903  elrsp  34031  qusrn  34064  elrspunidl  34082  elrspunsn  34083  selvply1rhmlema  34261  selvply1rhmlemb  34262  selvply1rhmlem3  34265  selvply1rhmlem4  34266  selvply1rhmlem5  34267  extvval  34274  extvfv  34276  extvfvcl  34279  extvfvalf  34280  mplvrpmfgalem  34287  mplvrpmga  34288  mplvrpmmhm  34289  mplvrpmrhm  34290  psrmonmul2  34294  issply  34304  esplyfvaln  34317  drgextgsum  34338  ply1degltdimlem  34365  fedgmullem2  34373  evls1fldgencl  34413  fldextrspunlsplem  34416  fldextrspunlsp  34417  extdgfialglem1  34435  extdgfialglem2  34436  minplyval  34448  ofcfval  34841  lpadval  35419  ptpconn  36206  bj-imdirvallem  38369  qmapex  39649  hashscontpow  43438  aks6d1c2  43446  sticksstones4  43465  sticksstones11  43472  sticksstones12a  43473  sticksstones12  43474  sticksstones17  43479  sticksstones18  43480  sticksstones19  43481  sticksstones20  43482  aks6d1c6lem2  43487  aks6d1c6lem3  43488  aks6d1c7lem2  43497  aks5lem2  43503  evlselv  43883  mhphf  43891  rfovfvd  45263  fsovfvd  45271  dssmapf1od  45282  choicefi  46487  axccdom  46508  climeldmeqmpt  46951  climfveqmpt  46954  climfveqmpt3  46965  climeldmeqmpt3  46972  climfveqmpt2  46976  climeldmeqmpt2  46978  climeqmpt  46980  limsupresicompt  47039  liminfresicompt  47063  liminfvalxr  47066  liminflbuz2  47098  iccvonmbllem  47961  vonioolem1  47963  vonioolem2  47964  vonicclem1  47966  vonicclem2  47967  smflimmpt  48093  smflimsuplem6  48108  cfsetsnfsetfv  48400  cfsetsnfsetf  48401  fundcmpsurbijinjpreimafv  48762  prproropen  48863  isubgr3stgr  49346  uspgrbispr  49522  1arymaptfv  50083  1arymaptfo  50086  fuco22  50792