Theorem mptexd 7236

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

Syntax hints:   → wi 4   ∈ wcel 2099  Vcvv 3471   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556

This theorem is referenced by:  mptsuppdifd  8191  mpocurryvald  8276  fsetfocdm  8880  fsuppssov1  9408  fsuppmptif  9423  sniffsupp  9424  cantnfrescl  9700  cantnflem1  9713  infxpenc2lem2  10044  ac5num  10060  ac6num  10503  negfi  12194  seqof2  14058  ramcl  16998  prdsplusgval  17455  prdsmulrval  17457  prdsvscaval  17461  galactghm  19359  gsum2dlem2  19926  gsum2d  19927  dprdfinv  19976  dprdfadd  19977  dmdprdsplitlem  19994  dpjfval  20012  dpjidcl  20015  mptscmfsupp0  20810  frlmgsum  21706  frlmphllem  21714  psrass1lemOLD  21874  psrass1lem  21877  psrridm  21906  psrcom  21911  mvrfval  21923  mplcoe5  21978  mplbas2  21980  evlslem6  22027  selvffval  22059  psdffval  22081  psdfval  22082  psdval  22083  psdmplcl  22086  psdmul  22090  evls1sca  22242  evls1fpws  22288  matgsum  22352  mvmulval  22458  mavmul0g  22468  marepvval0  22481  ptcnplem  23538  xkocnv  23731  ptcmplem3  23971  prdsdsf  24286  ressprdsds  24290  prdsxmslem2  24451  rrx0  25338  tdeglem4  26008  tdeglem4OLD  26009  pserulm  26371  efsubm  26498  addsuniflem  27931  suppovss  32478  mptiffisupp  32486  fsuppcurry1  32520  fsuppcurry2  32521  gsummptres2  32780  tocycval  32842  rmfsupp2  32959  elrsp  33098  qusrn  33132  elrspunidl  33157  elrspunsn  33158  drgextgsum  33294  ply1degltdimlem  33320  fedgmullem2  33328  evls1fldgencl  33358  minplyval  33376  ofcfval  33717  lpadval  34308  bj-imdirvallem  36659  hashscontpow  41593  aks6d1c2  41601  sticksstones4  41621  sticksstones11  41628  sticksstones12a  41629  sticksstones12  41630  sticksstones17  41635  sticksstones18  41636  sticksstones19  41637  sticksstones20  41638  aks6d1c6lem2  41643  aks6d1c6lem3  41644  aks6d1c7lem2  41653  evlsvvvallem  41794  evlsvvval  41796  selvvvval  41818  evlselv  41820  mhphf  41830  rfovfvd  43432  fsovfvd  43440  dssmapf1od  43451  choicefi  44573  axccdom  44595  climeldmeqmpt  45056  climfveqmpt  45059  climfveqmpt3  45070  climeldmeqmpt3  45077  climfveqmpt2  45081  climeldmeqmpt2  45083  climeqmpt  45085  limsupresicompt  45144  liminfresicompt  45168  liminfvalxr  45171  liminflbuz2  45203  iccvonmbllem  46066  vonioolem1  46068  vonioolem2  46069  vonicclem1  46071  vonicclem2  46072  smflimmpt  46198  smflimsuplem6  46213  cfsetsnfsetfv  46439  cfsetsnfsetf  46440  fundcmpsurbijinjpreimafv  46747  prproropen  46848  uspgrbispr  47213  1arymaptfv  47713  1arymaptfo  47716