Theorem mptexd 7222

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539

This theorem is used by:  mptsuppdifd  8187  mpocurryvald  8271  fsetfocdm  8867  fsuppssov1  9360  fsuppmptif  9375  sniffsupp  9376  cantnfrescl  9661  cantnflem1  9674  infxpenc2lem2  10080  ac5num  10096  ac6num  10538  negfi  12247  seqof2  14183  ramcl  17187  prdsplusgval  17624  prdsmulrval  17626  prdsvscaval  17630  galactghm  19598  gsum2dlem2  20165  gsum2d  20166  dprdfinv  20215  dprdfadd  20216  dmdprdsplitlem  20233  dpjfval  20251  dpjidcl  20254  mptscmfsupp0  21182  frlmgsum  22058  frlmphllem  22066  psrass1lem  22221  psrridm  22250  psrcom  22255  mvrfval  22268  mplcoe5  22329  mplbas2  22331  evlslem6  22370  evlsvvvallem  22380  evlsvvval  22382  selvffval  22407  selvvvval  22431  psdffval  22458  psdfval  22459  psdmplcl  22463  psdmul  22467  evls1sca  22621  evls1fpws  22667  matgsum  22732  mvmulval  22838  mavmul0g  22848  marepvval0  22861  ptcnplem  23920  xkocnv  24113  ptcmplem3  24353  prdsdsf  24666  ressprdsds  24670  prdsxmslem2  24828  rrx0  25698  tdeglem4  26358  pserulm  26731  efsubm  26861  addsuniflem  28369  suppovss  33256  fisuppov1  33258  mptiffisupp  33268  fsuppcurry1  33298  fsuppcurry2  33299  gsummptres2  33596  gsumfs2d  33604  tocycval  33651  rmfsupp2  33780  elrgspnlem2  33786  elrsp  33909  qusrn  33942  elrspunidl  33960  elrspunsn  33961  selvply1rhmlema  34132  selvply1rhmlemb  34133  selvply1rhmlem3  34136  selvply1rhmlem4  34137  selvply1rhmlem5  34138  extvval  34145  extvfv  34147  extvfvcl  34150  extvfvalf  34151  mplvrpmfgalem  34158  mplvrpmga  34159  mplvrpmmhm  34160  mplvrpmrhm  34161  psrmonmul2  34165  issply  34175  esplyfvaln  34188  drgextgsum  34209  ply1degltdimlem  34236  fedgmullem2  34244  evls1fldgencl  34284  fldextrspunlsplem  34287  fldextrspunlsp  34288  extdgfialglem1  34306  extdgfialglem2  34307  minplyval  34319  ofcfval  34712  lpadval  35291  bj-imdirvallem  38069  qmapex  39351  hashscontpow  43140  aks6d1c2  43148  sticksstones4  43167  sticksstones11  43174  sticksstones12a  43175  sticksstones12  43176  sticksstones17  43181  sticksstones18  43182  sticksstones19  43183  sticksstones20  43184  aks6d1c6lem2  43189  aks6d1c6lem3  43190  aks6d1c7lem2  43199  aks5lem2  43205  evlselv  43579  mhphf  43587  rfovfvd  44961  fsovfvd  44969  dssmapf1od  44980  choicefi  46157  axccdom  46178  climeldmeqmpt  46622  climfveqmpt  46625  climfveqmpt3  46636  climeldmeqmpt3  46643  climfveqmpt2  46647  climeldmeqmpt2  46649  climeqmpt  46651  limsupresicompt  46710  liminfresicompt  46734  liminfvalxr  46737  liminflbuz2  46769  iccvonmbllem  47632  vonioolem1  47634  vonioolem2  47635  vonicclem1  47637  vonicclem2  47638  smflimmpt  47764  smflimsuplem6  47779  cfsetsnfsetfv  48071  cfsetsnfsetf  48072  fundcmpsurbijinjpreimafv  48433  prproropen  48534  isubgr3stgr  49017  uspgrbispr  49193  1arymaptfv  49696  1arymaptfo  49699  fuco22  50391