Theorem mptexd 6981

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3494   ↦ cmpt 5138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357

This theorem is referenced by:  mptsuppdifd  7846  mpocurryvald  7930  fsuppmptif  8857  sniffsupp  8867  cantnfrescl  9133  cantnflem1  9146  infxpenc2lem2  9440  ac5num  9456  ac6num  9895  negfi  11583  seqof2  13422  ramcl  16359  prdsplusgval  16740  prdsmulrval  16742  prdsvscaval  16746  galactghm  18526  gsum2dlem2  19085  gsum2d  19086  dprdfinv  19135  dprdfadd  19136  dmdprdsplitlem  19153  dpjfval  19171  dpjidcl  19174  mptscmfsupp0  19693  psrass1lem  20151  psrridm  20178  psrcom  20183  mvrfval  20194  mplcoe5  20243  mplbas2  20245  evlslem6  20288  selvffval  20323  evls1sca  20480  frlmgsum  20910  frlmphllem  20918  matgsum  21040  mvmulval  21146  mavmul0g  21156  marepvval0  21169  ptcnplem  22223  xkocnv  22416  ptcmplem3  22656  prdsdsf  22971  ressprdsds  22975  prdsxmslem2  23133  rrx0  23994  tdeglem4  24648  pserulm  25004  efsubm  25129  suppovss  30420  fsuppcurry1  30455  fsuppcurry2  30456  tocycval  30745  rmfsupp2  30861  drgextgsum  30992  fedgmullem2  31021  ofcfval  31352  lpadval  31942  bj-imdirval  34466  rfovfvd  40341  fsovfvd  40349  dssmapf1od  40360  choicefi  41456  axccdom  41480  climeldmeqmpt  41942  climfveqmpt  41945  climfveqmpt3  41956  climeldmeqmpt3  41963  climfveqmpt2  41967  climeldmeqmpt2  41969  climeqmpt  41971  limsupresicompt  42030  liminfresicompt  42054  liminfvalxr  42057  liminflbuz2  42089  iccvonmbllem  42954  vonioolem1  42956  vonioolem2  42957  vonicclem1  42959  vonicclem2  42960  smflimmpt  43078  smflimsuplem6  43093  fundcmpsurbijinjpreimafv  43561  prproropen  43664  uspgrbispr  44020