Theorem mptexd 7231

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547

This theorem is used by:  mptsuppdifd  8207  mpocurryvald  8291  fsetfocdm  8887  fsuppssov1  9380  fsuppmptif  9395  sniffsupp  9396  cantnfrescl  9681  cantnflem1  9694  infxpenc2lem2  10103  ac5num  10119  ac6num  10561  negfi  12270  seqof2  14207  ramcl  17213  prdsplusgval  17650  prdsmulrval  17652  prdsvscaval  17656  galactghm  19624  gsum2dlem2  20191  gsum2d  20192  dprdfinv  20241  dprdfadd  20242  dmdprdsplitlem  20259  dpjfval  20277  dpjidcl  20280  mptscmfsupp0  21208  frlmgsum  22084  frlmphllem  22092  psrass1lem  22247  psrridm  22276  psrcom  22281  mvrfval  22294  mplcoe5  22355  mplbas2  22357  evlslem6  22396  evlsvvvallem  22406  evlsvvval  22408  selvffval  22433  selvvvval  22457  psdffval  22484  psdfval  22485  psdmplcl  22489  psdmul  22493  evls1sca  22647  evls1fpws  22693  matgsum  22758  mvmulval  22864  mavmul0g  22874  marepvval0  22887  ptcnplem  23946  xkocnv  24139  ptcmplem3  24379  prdsdsf  24692  ressprdsds  24696  prdsxmslem2  24854  rrx0  25724  tdeglem4  26384  pserulm  26755  efsubm  26885  addsuniflem  28393  suppovss  33322  fisuppov1  33324  mptiffisupp  33334  fsuppcurry1  33363  fsuppcurry2  33364  gsummptres2  33661  gsumfs2d  33669  tocycval  33716  rmfsupp2  33845  elrgspnlem2  33851  elrsp  33974  qusrn  34007  elrspunidl  34025  elrspunsn  34026  selvply1rhmlema  34197  selvply1rhmlemb  34198  selvply1rhmlem3  34201  selvply1rhmlem4  34202  selvply1rhmlem5  34203  extvval  34210  extvfv  34212  extvfvcl  34215  extvfvalf  34216  mplvrpmfgalem  34223  mplvrpmga  34224  mplvrpmmhm  34225  mplvrpmrhm  34226  psrmonmul2  34230  issply  34240  esplyfvaln  34253  drgextgsum  34274  ply1degltdimlem  34301  fedgmullem2  34309  evls1fldgencl  34349  fldextrspunlsplem  34352  fldextrspunlsp  34353  extdgfialglem1  34371  extdgfialglem2  34372  minplyval  34384  ofcfval  34777  lpadval  35355  ptpconn  36085  bj-imdirvallem  38195  qmapex  39477  hashscontpow  43266  aks6d1c2  43274  sticksstones4  43293  sticksstones11  43300  sticksstones12a  43301  sticksstones12  43302  sticksstones17  43307  sticksstones18  43308  sticksstones19  43309  sticksstones20  43310  aks6d1c6lem2  43315  aks6d1c6lem3  43316  aks6d1c7lem2  43325  aks5lem2  43331  evlselv  43711  mhphf  43719  rfovfvd  45096  fsovfvd  45104  dssmapf1od  45115  choicefi  46308  axccdom  46329  climeldmeqmpt  46772  climfveqmpt  46775  climfveqmpt3  46786  climeldmeqmpt3  46793  climfveqmpt2  46797  climeldmeqmpt2  46799  climeqmpt  46801  limsupresicompt  46860  liminfresicompt  46884  liminfvalxr  46887  liminflbuz2  46919  iccvonmbllem  47782  vonioolem1  47784  vonioolem2  47785  vonicclem1  47787  vonicclem2  47788  smflimmpt  47914  smflimsuplem6  47929  cfsetsnfsetfv  48221  cfsetsnfsetf  48222  fundcmpsurbijinjpreimafv  48583  prproropen  48684  isubgr3stgr  49167  uspgrbispr  49343  1arymaptfv  49846  1arymaptfo  49849  fuco22  50555