Theorem mptexd 7216

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459   ↦ cmpt 5201

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539

This theorem is referenced by:  mptsuppdifd  8185  mpocurryvald  8269  fsetfocdm  8875  fsuppssov1  9396  fsuppmptif  9411  sniffsupp  9412  cantnfrescl  9690  cantnflem1  9703  infxpenc2lem2  10034  ac5num  10050  ac6num  10493  negfi  12191  seqof2  14078  ramcl  17049  prdsplusgval  17487  prdsmulrval  17489  prdsvscaval  17493  galactghm  19385  gsum2dlem2  19952  gsum2d  19953  dprdfinv  20002  dprdfadd  20003  dmdprdsplitlem  20020  dpjfval  20038  dpjidcl  20041  mptscmfsupp0  20884  frlmgsum  21732  frlmphllem  21740  psrass1lem  21892  psrridm  21923  psrcom  21928  mvrfval  21941  mplcoe5  21998  mplbas2  22000  evlslem6  22039  selvffval  22071  psdffval  22095  psdfval  22096  psdmplcl  22100  psdmul  22104  evls1sca  22261  evls1fpws  22307  matgsum  22375  mvmulval  22481  mavmul0g  22491  marepvval0  22504  ptcnplem  23559  xkocnv  23752  ptcmplem3  23992  prdsdsf  24306  ressprdsds  24310  prdsxmslem2  24468  rrx0  25349  tdeglem4  26017  pserulm  26383  efsubm  26512  addsuniflem  27960  suppovss  32658  fisuppov1  32660  mptiffisupp  32670  fsuppcurry1  32702  fsuppcurry2  32703  gsummptres2  33047  gsumfs2d  33049  tocycval  33119  rmfsupp2  33233  elrgspnlem2  33238  elrsp  33387  qusrn  33424  elrspunidl  33443  elrspunsn  33444  drgextgsum  33634  ply1degltdimlem  33662  fedgmullem2  33670  evls1fldgencl  33711  fldextrspunlsplem  33714  fldextrspunlsp  33715  minplyval  33739  ofcfval  34129  lpadval  34708  bj-imdirvallem  37198  hashscontpow  42135  aks6d1c2  42143  sticksstones4  42162  sticksstones11  42169  sticksstones12a  42170  sticksstones12  42171  sticksstones17  42176  sticksstones18  42177  sticksstones19  42178  sticksstones20  42179  aks6d1c6lem2  42184  aks6d1c6lem3  42185  aks6d1c7lem2  42194  aks5lem2  42200  evlsvvvallem  42584  evlsvvval  42586  selvvvval  42608  evlselv  42610  mhphf  42620  rfovfvd  44026  fsovfvd  44034  dssmapf1od  44045  choicefi  45224  axccdom  45246  climeldmeqmpt  45697  climfveqmpt  45700  climfveqmpt3  45711  climeldmeqmpt3  45718  climfveqmpt2  45722  climeldmeqmpt2  45724  climeqmpt  45726  limsupresicompt  45785  liminfresicompt  45809  liminfvalxr  45812  liminflbuz2  45844  iccvonmbllem  46707  vonioolem1  46709  vonioolem2  46710  vonicclem1  46712  vonicclem2  46713  smflimmpt  46839  smflimsuplem6  46854  cfsetsnfsetfv  47086  cfsetsnfsetf  47087  fundcmpsurbijinjpreimafv  47421  prproropen  47522  isubgr3stgr  47987  uspgrbispr  48126  1arymaptfv  48620  1arymaptfo  48623  fuco22  49250