Theorem mptexd 7175

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3432   ↦ cmpt 5160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500

This theorem is referenced by:  mptsuppdifd  8133  mpocurryvald  8217  fsetfocdm  8805  fsuppssov1  9294  fsuppmptif  9309  sniffsupp  9310  cantnfrescl  9595  cantnflem1  9608  infxpenc2lem2  9940  ac5num  9956  ac6num  10399  negfi  12103  seqof2  14020  ramcl  16998  prdsplusgval  17434  prdsmulrval  17436  prdsvscaval  17440  galactghm  19377  gsum2dlem2  19944  gsum2d  19945  dprdfinv  19994  dprdfadd  19995  dmdprdsplitlem  20012  dpjfval  20030  dpjidcl  20033  mptscmfsupp0  20924  frlmgsum  21754  frlmphllem  21762  psrass1lem  21915  psrridm  21944  psrcom  21949  mvrfval  21962  mplcoe5  22023  mplbas2  22025  evlslem6  22064  evlsvvvallem  22074  evlsvvval  22076  selvffval  22101  selvvvval  22125  psdffval  22152  psdfval  22153  psdmplcl  22157  psdmul  22161  evls1sca  22316  evls1fpws  22362  matgsum  22427  mvmulval  22533  mavmul0g  22543  marepvval0  22556  ptcnplem  23611  xkocnv  23804  ptcmplem3  24044  prdsdsf  24357  ressprdsds  24361  prdsxmslem2  24519  rrx0  25389  tdeglem4  26050  pserulm  26412  efsubm  26540  addsuniflem  28018  suppovss  32780  fisuppov1  32782  mptiffisupp  32792  fsuppcurry1  32823  fsuppcurry2  32824  gsummptres2  33141  gsumfs2d  33149  tocycval  33196  rmfsupp2  33326  elrgspnlem2  33331  elrsp  33462  qusrn  33499  elrspunidl  33518  elrspunsn  33519  selvply1rhmlema  33709  selvply1rhmlemb  33710  selvply1rhmlem3  33713  selvply1rhmlem4  33714  selvply1rhmlem5  33715  extvval  33722  extvfv  33724  extvfvcl  33727  extvfvalf  33728  mplvrpmfgalem  33735  mplvrpmga  33736  mplvrpmmhm  33737  mplvrpmrhm  33738  psrmonmul2  33742  issply  33752  esplyfvaln  33765  drgextgsum  33786  ply1degltdimlem  33813  fedgmullem2  33821  evls1fldgencl  33861  fldextrspunlsplem  33864  fldextrspunlsp  33865  extdgfialglem1  33883  extdgfialglem2  33884  minplyval  33896  ofcfval  34289  lpadval  34867  bj-imdirvallem  37547  qmapex  38825  hashscontpow  42614  aks6d1c2  42622  sticksstones4  42641  sticksstones11  42648  sticksstones12a  42649  sticksstones12  42650  sticksstones17  42655  sticksstones18  42656  sticksstones19  42657  sticksstones20  42658  aks6d1c6lem2  42663  aks6d1c6lem3  42664  aks6d1c7lem2  42673  aks5lem2  42679  evlselv  43046  mhphf  43054  rfovfvd  44453  fsovfvd  44461  dssmapf1od  44472  choicefi  45653  axccdom  45674  climeldmeqmpt  46118  climfveqmpt  46121  climfveqmpt3  46132  climeldmeqmpt3  46139  climfveqmpt2  46143  climeldmeqmpt2  46145  climeqmpt  46147  limsupresicompt  46206  liminfresicompt  46230  liminfvalxr  46233  liminflbuz2  46265  iccvonmbllem  47128  vonioolem1  47130  vonioolem2  47131  vonicclem1  47133  vonicclem2  47134  smflimmpt  47260  smflimsuplem6  47275  cfsetsnfsetfv  47527  cfsetsnfsetf  47528  fundcmpsurbijinjpreimafv  47889  prproropen  47990  isubgr3stgr  48473  uspgrbispr  48649  1arymaptfv  49138  1arymaptfo  49141  fuco22  49836