Theorem mptexg 7079

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 6456	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2738	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6133	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5242	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 686	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 7077	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 586	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422   ⊆ wss 3883   ↦ cmpt 5153  dom cdm 5580  Fun wfun 6412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426

This theorem is referenced by:  mptex  7081  mptexd  7082  ovmpt3rab1  7505  offval  7520  abrexexg  7777  xpexgALT  7797  offval3  7798  suppssov1  7985  suppssfv  7989  iunon  8141  onoviun  8145  mptelixpg  8681  cantnfp1lem1  9366  updjud  9623  coftr  9960  axcc3  10125  reps  14411  wrd2f1tovbij  14603  restval  17054  resf1st  17525  resf2nd  17526  funcres  17527  vrmdfval  18410  symgfixfolem1  18961  pmtrval  18974  pmtrrn  18980  pmtrfrn  18981  sylow1lem4  19121  sylow3lem2  19148  sylow3lem3  19149  uvcfval  20901  uvcval  20902  uvcff  20908  uvcresum  20910  psrass1lemOLD  21053  psrass1lem  21056  opsrval  21157  selvfval  21237  psropprmul  21319  mavmuldm  21607  mat2pmatfval  21780  cpm2mfval  21806  chpmatfval  21887  ntrfval  22083  clsfval  22084  neifval  22158  lpfval  22197  ptcnplem  22680  upxp  22682  fmfnfmlem3  23015  fmfnfmlem4  23016  ustuqtoplem  23299  ustuqtop0  23300  utopsnneiplem  23307  rrxmval  24474  tdeglem4OLD  25130  tayl0  25426  itgulm2  25473  efabl  25611  tgjustr  26739  lmif  27050  islmib  27052  nbusgrf1o1  27640  cusgrfilem3  27727  vtxdgfval  27737  wlkiswwlks2  28141  wwlksnextbij  28168  clwlkclwwlklem1  28264  grpoinvfval  28785  acunirnmpt  30898  acunirnmpt2  30899  acunirnmpt2f  30900  aciunf1lem  30901  fnpreimac  30910  frlmdim  31596  indv  31880  indval  31881  ofcfval3  31970  omsval  32160  carsgclctunlem2  32186  pmeasadd  32192  sitgclg  32209  bnj1366  32709  ptpconn  33095  fwddifval  34391  tailfval  34488  curfv  35684  matunitlindflem1  35700  matunitlindflem2  35701  upixp  35814  pw2f1ocnv  40775  kelac1  40804  rfovd  41498  fsovrfovd  41506  dssmapfvd  41514  dssmapfv2d  41515  fmulcl  43012  fmuldfeqlem1  43013  dvnmul  43374  dvnprodlem2  43378  stoweidlem31  43462  stoweidlem42  43473  stoweidlem48  43479  etransclem1  43666  etransclem4  43669  etransclem13  43678  etransclem17  43682  0ome  43957  hoicvr  43976  hsphoif  44004  hsphoival  44007  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoilem1  44029  ovnhoilem2  44030  ovnlecvr2  44038  ovncvr2  44039  hoidifhspval2  44043  hspmbllem2  44055  fundcmpsurinjALT  44752  sprbisymrel  44839  uspgrbisymrelALT  45205  funcrngcsetc  45444  funcringcsetc  45481  scmsuppss  45596  rmfsupp  45598  scmfsupp  45602  mptcfsupp  45604  lincresunit2  45707  itcoval0mpt  45900  eufsn  46057