Theorem mptexd 7164

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3438   ↦ cmpt 5176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494

This theorem is referenced by:  mptsuppdifd  8126  mpocurryvald  8210  fsetfocdm  8795  fsuppssov1  9293  fsuppmptif  9308  sniffsupp  9309  cantnfrescl  9591  cantnflem1  9604  infxpenc2lem2  9933  ac5num  9949  ac6num  10392  negfi  12092  seqof2  13985  ramcl  16959  prdsplusgval  17395  prdsmulrval  17397  prdsvscaval  17401  galactghm  19301  gsum2dlem2  19868  gsum2d  19869  dprdfinv  19918  dprdfadd  19919  dmdprdsplitlem  19936  dpjfval  19954  dpjidcl  19957  mptscmfsupp0  20848  frlmgsum  21697  frlmphllem  21705  psrass1lem  21857  psrridm  21888  psrcom  21893  mvrfval  21906  mplcoe5  21963  mplbas2  21965  evlslem6  22004  selvffval  22036  psdffval  22060  psdfval  22061  psdmplcl  22065  psdmul  22069  evls1sca  22226  evls1fpws  22272  matgsum  22340  mvmulval  22446  mavmul0g  22456  marepvval0  22469  ptcnplem  23524  xkocnv  23717  ptcmplem3  23957  prdsdsf  24271  ressprdsds  24275  prdsxmslem2  24433  rrx0  25313  tdeglem4  25981  pserulm  26347  efsubm  26476  addsuniflem  27931  suppovss  32637  fisuppov1  32639  mptiffisupp  32649  fsuppcurry1  32681  fsuppcurry2  32682  gsummptres2  33019  gsumfs2d  33021  tocycval  33063  rmfsupp2  33188  elrgspnlem2  33193  elrsp  33319  qusrn  33356  elrspunidl  33375  elrspunsn  33376  drgextgsum  33566  ply1degltdimlem  33594  fedgmullem2  33602  evls1fldgencl  33641  fldextrspunlsplem  33644  fldextrspunlsp  33645  minplyval  33671  ofcfval  34064  lpadval  34643  bj-imdirvallem  37153  hashscontpow  42095  aks6d1c2  42103  sticksstones4  42122  sticksstones11  42129  sticksstones12a  42130  sticksstones12  42131  sticksstones17  42136  sticksstones18  42137  sticksstones19  42138  sticksstones20  42139  aks6d1c6lem2  42144  aks6d1c6lem3  42145  aks6d1c7lem2  42154  aks5lem2  42160  evlsvvvallem  42534  evlsvvval  42536  selvvvval  42558  evlselv  42560  mhphf  42570  rfovfvd  43975  fsovfvd  43983  dssmapf1od  43994  choicefi  45178  axccdom  45200  climeldmeqmpt  45650  climfveqmpt  45653  climfveqmpt3  45664  climeldmeqmpt3  45671  climfveqmpt2  45675  climeldmeqmpt2  45677  climeqmpt  45679  limsupresicompt  45738  liminfresicompt  45762  liminfvalxr  45765  liminflbuz2  45797  iccvonmbllem  46660  vonioolem1  46662  vonioolem2  46663  vonicclem1  46665  vonicclem2  46666  smflimmpt  46792  smflimsuplem6  46807  cfsetsnfsetfv  47042  cfsetsnfsetf  47043  fundcmpsurbijinjpreimafv  47392  prproropen  47493  isubgr3stgr  47960  uspgrbispr  48136  1arymaptfv  48626  1arymaptfo  48629  fuco22  49325