Theorem mptexd 6964

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441   ↦ cmpt 5110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332

This theorem is referenced by:  mptsuppdifd  7835  mpocurryvald  7919  fsuppmptif  8847  sniffsupp  8857  cantnfrescl  9123  cantnflem1  9136  infxpenc2lem2  9431  ac5num  9447  ac6num  9890  negfi  11577  seqof2  13424  ramcl  16355  prdsplusgval  16738  prdsmulrval  16740  prdsvscaval  16744  galactghm  18524  gsum2dlem2  19084  gsum2d  19085  dprdfinv  19134  dprdfadd  19135  dmdprdsplitlem  19152  dpjfval  19170  dpjidcl  19173  mptscmfsupp0  19692  frlmgsum  20461  frlmphllem  20469  psrass1lem  20615  psrridm  20642  psrcom  20647  mvrfval  20658  mplcoe5  20708  mplbas2  20710  evlslem6  20753  selvffval  20788  evls1sca  20947  matgsum  21042  mvmulval  21148  mavmul0g  21158  marepvval0  21171  ptcnplem  22226  xkocnv  22419  ptcmplem3  22659  prdsdsf  22974  ressprdsds  22978  prdsxmslem2  23136  rrx0  24001  tdeglem4  24661  pserulm  25017  efsubm  25143  suppovss  30443  fsuppcurry1  30487  fsuppcurry2  30488  gsummptres2  30738  tocycval  30800  rmfsupp2  30917  elrsp  30989  elrspunidl  31014  drgextgsum  31085  fedgmullem2  31114  ofcfval  31467  lpadval  32057  bj-imdirvallem  34595  rfovfvd  40703  fsovfvd  40711  dssmapf1od  40722  choicefi  41829  axccdom  41853  climeldmeqmpt  42310  climfveqmpt  42313  climfveqmpt3  42324  climeldmeqmpt3  42331  climfveqmpt2  42335  climeldmeqmpt2  42337  climeqmpt  42339  limsupresicompt  42398  liminfresicompt  42422  liminfvalxr  42425  liminflbuz2  42457  iccvonmbllem  43317  vonioolem1  43319  vonioolem2  43320  vonicclem1  43322  vonicclem2  43323  smflimmpt  43441  smflimsuplem6  43456  fundcmpsurbijinjpreimafv  43924  prproropen  44025  uspgrbispr  44379  1arymaptfv  45054  1arymaptfo  45057