Theorem mptexg 7177

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 6538	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2737	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6207	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5270	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 691	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 7175	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 588	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903   ↦ cmpt 5181  dom cdm 5632  Fun wfun 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508

This theorem is referenced by:  mptex  7179  mptexd  7180  ovmpt3rab1  7626  offval  7641  xpexgALT  7935  offval3  7936  suppssov1  8149  suppssov2  8150  suppssfv  8154  iunon  8281  onoviun  8285  mptelixpg  8885  cantnfp1lem1  9599  updjud  9858  coftr  10195  axcc3  10360  reps  14705  wrd2f1tovbij  14895  restval  17358  resf1st  17830  resf2nd  17831  funcres  17832  vrmdfval  18793  symgfixfolem1  19379  pmtrval  19392  pmtrrn  19398  pmtrfrn  19399  sylow1lem4  19542  sylow3lem2  19569  sylow3lem3  19570  funcrngcsetc  20585  funcringcsetc  20619  uvcfval  21751  uvcval  21752  uvcff  21758  uvcresum  21760  psrass1lem  21900  opsrval  22013  selvfval  22089  psropprmul  22190  mavmuldm  22506  mat2pmatfval  22679  cpm2mfval  22705  chpmatfval  22786  ntrfval  22980  clsfval  22981  neifval  23055  lpfval  23094  ptcnplem  23577  upxp  23579  fmfnfmlem3  23912  fmfnfmlem4  23913  ustuqtoplem  24195  ustuqtop0  24196  utopsnneiplem  24203  rrxmval  25373  tayl0  26337  itgulm2  26386  efabl  26527  tgjustr  28558  lmif  28869  islmib  28871  nbusgrf1o1  29455  cusgrfilem3  29543  vtxdgfval  29553  wlkiswwlks2  29960  wwlksnextbij  29987  clwlkclwwlklem1  30086  grpoinvfval  30609  acunirnmpt  32748  acunirnmpt2  32749  acunirnmpt2f  32750  aciunf1lem  32751  fnpreimac  32759  mptiffisupp  32782  indv  32941  indval  32942  frlmdim  33788  ofcfval3  34279  omsval  34470  carsgclctunlem2  34496  pmeasadd  34502  sitgclg  34519  bnj1366  35004  ptpconn  35446  fwddifval  36375  tailfval  36585  curfv  37845  matunitlindflem1  37861  matunitlindflem2  37862  upixp  37974  pw2f1ocnv  43388  kelac1  43414  rfovd  44351  fsovrfovd  44359  dssmapfvd  44367  dssmapfv2d  44368  fmulcl  45935  fmuldfeqlem1  45936  dvnmul  46295  dvnprodlem2  46299  stoweidlem31  46383  stoweidlem42  46394  stoweidlem48  46400  etransclem1  46587  etransclem4  46590  etransclem13  46599  etransclem17  46603  0ome  46881  hoicvr  46900  hsphoif  46928  hsphoival  46931  hoidmvlelem2  46948  hoidmvlelem3  46949  ovnhoilem1  46953  ovnhoilem2  46954  ovnlecvr2  46962  ovncvr2  46963  hoidifhspval2  46967  hspmbllem2  46979  fundcmpsurinjALT  47766  sprbisymrel  47853  uspgrbisymrelALT  48509  scmsuppss  48725  rmfsupp  48727  scmfsupp  48729  mptcfsupp  48731  lincresunit2  48832  itcoval0mpt  49020  eufsn  49195