Theorem mptexg 6389

Description: If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)

Assertion

Ref	Expression
mptexg	⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem mptexg

Step	Hyp	Ref	Expression
1		funmpt 5840	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2610	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 5548	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 4732	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 702	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 6387	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 694	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540   ↦ cmpt 4643  dom cdm 5038  Fun wfun 5798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812

This theorem is referenced by:  mptex  6390  mptexd  6391  ovmpt3rab1  6789  offval  6802  abrexexg  7034  xpexgALT  7052  offval3  7053  mptsuppdifd  7204  suppssov1  7214  suppssfv  7218  mpt2curryvald  7283  iunon  7323  onoviun  7327  mptelixpg  7831  fsuppmptif  8188  sniffsupp  8198  cantnfrescl  8456  cantnfp1lem1  8458  cantnflem1  8469  infxpenc2lem2  8726  coftr  8978  axcc3  9143  negfi  10850  seqof2  12721  reps  13368  wrd2f1tovbij  13551  ramcl  15571  restval  15910  prdsplusgval  15956  prdsmulrval  15958  prdsvscaval  15962  resf1st  16377  resf2nd  16378  funcres  16379  galactghm  17646  symgfixfolem1  17681  pmtrval  17694  pmtrrn  17700  pmtrfrn  17701  sylow1lem4  17839  sylow3lem2  17866  sylow3lem3  17867  gsum2dlem2  18193  gsum2d  18194  dprdfinv  18241  dprdfadd  18242  dmdprdsplitlem  18259  dpjfval  18277  dpjidcl  18280  mptscmfsupp0  18751  psrass1lem  19198  psrridm  19225  psrcom  19230  mvrfval  19241  mplcoe5  19289  mplbas2  19291  opsrval  19295  evlslem6  19334  psropprmul  19429  evls1sca  19509  frlmgsum  19930  frlmphllem  19938  uvcfval  19942  uvcval  19943  uvcff  19949  uvcresum  19951  matgsum  20062  mvmulval  20168  mavmuldm  20175  mavmul0g  20178  marepvval0  20191  mat2pmatfval  20347  cpm2mfval  20373  chpmatfval  20454  ntrfval  20638  clsfval  20639  neifval  20713  lpfval  20752  ptcnplem  21234  upxp  21236  xkocnv  21427  fmfnfmlem3  21570  fmfnfmlem4  21571  ptcmplem3  21668  ustuqtoplem  21853  ustuqtop0  21854  utopsnneiplem  21861  prdsdsf  21982  ressprdsds  21986  prdsxmslem2  22144  rrxmval  22996  tdeglem4  23624  tayl0  23920  itgulm2  23967  pserulm  23980  efabl  24100  efsubm  24101  lmif  25477  islmib  25479  nbgraf1o0  25975  cusgrafilem3  26009  wlkiswwlk2  26225  wwlkextbij  26261  clwlkisclwwlklem2  26314  vdgrfval  26422  frgrancvvdeqlem9  26568  grpoinvfval  26760  acunirnmpt  28841  acunirnmpt2  28842  acunirnmpt2f  28843  aciunf1lem  28844  indv  29402  indval  29403  ofcfval  29487  ofcfval3  29491  omsval  29682  carsgclctunlem2  29708  pmeasadd  29714  sitgclg  29731  bnj1366  30154  ptpcon  30469  fwddifval  31439  tailfval  31537  curfv  32559  matunitlindflem1  32575  matunitlindflem2  32576  upixp  32694  pw2f1ocnv  36622  kelac1  36651  rfovd  37315  rfovfvd  37316  fsovrfovd  37323  fsovfvd  37324  dssmapfvd  37331  dssmapfv2d  37332  dssmapf1od  37335  fmulcl  38648  fmuldfeqlem1  38649  dvnmul  38833  dvnprodlem2  38837  stoweidlem31  38924  stoweidlem42  38935  stoweidlem48  38941  etransclem1  39128  etransclem4  39131  etransclem13  39140  etransclem17  39144  0ome  39419  hoicvr  39438  hsphoif  39466  hsphoival  39469  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoilem1  39491  ovnhoilem2  39492  ovnlecvr2  39500  ovncvr2  39501  hoidifhspval2  39505  hspmbllem2  39517  nbusgrf1o1  40598  cusgrfilem3  40673  vtxdgfval  40683  1wlkiswwlks2  41072  wwlksnextbij  41108  clwlkclwwlklem1  41208  funcrngcsetc  41790  funcringcsetc  41827  scmsuppss  41947  rmfsupp  41949  scmfsupp  41953  mptcfsupp  41955  lincresunit2  42061  offval0  42093