Theorem mptexd 7227

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

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

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 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545

This theorem is used by:  mptsuppdifd  8188  mpocurryvald  8272  fsetfocdm  8866  fsuppssov1  9358  fsuppmptif  9373  sniffsupp  9374  cantnfrescl  9659  cantnflem1  9672  infxpenc2lem2  10027  ac5num  10043  ac6num  10485  negfi  12192  seqof2  14128  ramcl  17127  prdsplusgval  17564  prdsmulrval  17566  prdsvscaval  17570  galactghm  19537  gsum2dlem2  20104  gsum2d  20105  dprdfinv  20154  dprdfadd  20155  dmdprdsplitlem  20172  dpjfval  20190  dpjidcl  20193  mptscmfsupp0  21117  frlmgsum  21991  frlmphllem  21999  psrass1lem  22154  psrridm  22183  psrcom  22188  mvrfval  22201  mplcoe5  22262  mplbas2  22264  evlslem6  22303  evlsvvvallem  22313  evlsvvval  22315  selvffval  22340  selvvvval  22364  psdffval  22391  psdfval  22392  psdmplcl  22396  psdmul  22400  evls1sca  22554  evls1fpws  22600  matgsum  22665  mvmulval  22771  mavmul0g  22781  marepvval0  22794  ptcnplem  23853  xkocnv  24046  ptcmplem3  24286  prdsdsf  24599  ressprdsds  24603  prdsxmslem2  24761  rrx0  25631  tdeglem4  26292  pserulm  26665  efsubm  26796  addsuniflem  28274  suppovss  33161  fisuppov1  33163  mptiffisupp  33173  fsuppcurry1  33203  fsuppcurry2  33204  gsummptres2  33501  gsumfs2d  33509  tocycval  33556  rmfsupp2  33685  elrgspnlem2  33691  elrsp  33814  qusrn  33846  elrspunidl  33864  elrspunsn  33865  selvply1rhmlema  34036  selvply1rhmlemb  34037  selvply1rhmlem3  34040  selvply1rhmlem4  34041  selvply1rhmlem5  34042  extvval  34049  extvfv  34051  extvfvcl  34054  extvfvalf  34055  mplvrpmfgalem  34062  mplvrpmga  34063  mplvrpmmhm  34064  mplvrpmrhm  34065  psrmonmul2  34069  issply  34079  esplyfvaln  34092  drgextgsum  34113  ply1degltdimlem  34140  fedgmullem2  34148  evls1fldgencl  34188  fldextrspunlsplem  34191  fldextrspunlsp  34192  extdgfialglem1  34210  extdgfialglem2  34211  minplyval  34223  ofcfval  34616  lpadval  35195  bj-imdirvallem  37940  qmapex  39207  hashscontpow  42996  aks6d1c2  43004  sticksstones4  43023  sticksstones11  43030  sticksstones12a  43031  sticksstones12  43032  sticksstones17  43037  sticksstones18  43038  sticksstones19  43039  sticksstones20  43040  aks6d1c6lem2  43045  aks6d1c6lem3  43046  aks6d1c7lem2  43055  aks5lem2  43061  evlselv  43443  mhphf  43451  rfovfvd  44850  fsovfvd  44858  dssmapf1od  44869  choicefi  46039  axccdom  46060  climeldmeqmpt  46504  climfveqmpt  46507  climfveqmpt3  46518  climeldmeqmpt3  46525  climfveqmpt2  46529  climeldmeqmpt2  46531  climeqmpt  46533  limsupresicompt  46592  liminfresicompt  46616  liminfvalxr  46619  liminflbuz2  46651  iccvonmbllem  47514  vonioolem1  47516  vonioolem2  47517  vonicclem1  47519  vonicclem2  47520  smflimmpt  47646  smflimsuplem6  47661  cfsetsnfsetfv  47953  cfsetsnfsetf  47954  fundcmpsurbijinjpreimafv  48315  prproropen  48416  isubgr3stgr  48899  uspgrbispr  49075  1arymaptfv  49578  1arymaptfo  49581  fuco22  50273