Theorem mptexg 7097

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 6472	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2738	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6144	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5247	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 687	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 7095	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 587	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3432   ⊆ wss 3887   ↦ cmpt 5157  dom cdm 5589  Fun wfun 6427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441

This theorem is referenced by:  mptex  7099  mptexd  7100  ovmpt3rab1  7527  offval  7542  abrexexgOLD  7804  xpexgALT  7824  offval3  7825  suppssov1  8014  suppssfv  8018  iunon  8170  onoviun  8174  mptelixpg  8723  cantnfp1lem1  9436  updjud  9692  coftr  10029  axcc3  10194  reps  14483  wrd2f1tovbij  14675  restval  17137  resf1st  17609  resf2nd  17610  funcres  17611  vrmdfval  18495  symgfixfolem1  19046  pmtrval  19059  pmtrrn  19065  pmtrfrn  19066  sylow1lem4  19206  sylow3lem2  19233  sylow3lem3  19234  uvcfval  20991  uvcval  20992  uvcff  20998  uvcresum  21000  psrass1lemOLD  21143  psrass1lem  21146  opsrval  21247  selvfval  21327  psropprmul  21409  mavmuldm  21699  mat2pmatfval  21872  cpm2mfval  21898  chpmatfval  21979  ntrfval  22175  clsfval  22176  neifval  22250  lpfval  22289  ptcnplem  22772  upxp  22774  fmfnfmlem3  23107  fmfnfmlem4  23108  ustuqtoplem  23391  ustuqtop0  23392  utopsnneiplem  23399  rrxmval  24569  tdeglem4OLD  25225  tayl0  25521  itgulm2  25568  efabl  25706  tgjustr  26835  lmif  27146  islmib  27148  nbusgrf1o1  27737  cusgrfilem3  27824  vtxdgfval  27834  wlkiswwlks2  28240  wwlksnextbij  28267  clwlkclwwlklem1  28363  grpoinvfval  28884  acunirnmpt  30996  acunirnmpt2  30997  acunirnmpt2f  30998  aciunf1lem  30999  fnpreimac  31008  frlmdim  31694  indv  31980  indval  31981  ofcfval3  32070  omsval  32260  carsgclctunlem2  32286  pmeasadd  32292  sitgclg  32309  bnj1366  32809  ptpconn  33195  fwddifval  34464  tailfval  34561  curfv  35757  matunitlindflem1  35773  matunitlindflem2  35774  upixp  35887  pw2f1ocnv  40859  kelac1  40888  rfovd  41609  fsovrfovd  41617  dssmapfvd  41625  dssmapfv2d  41626  fmulcl  43122  fmuldfeqlem1  43123  dvnmul  43484  dvnprodlem2  43488  stoweidlem31  43572  stoweidlem42  43583  stoweidlem48  43589  etransclem1  43776  etransclem4  43779  etransclem13  43788  etransclem17  43792  0ome  44067  hoicvr  44086  hsphoif  44114  hsphoival  44117  hoidmvlelem2  44134  hoidmvlelem3  44135  ovnhoilem1  44139  ovnhoilem2  44140  ovnlecvr2  44148  ovncvr2  44149  hoidifhspval2  44153  hspmbllem2  44165  fundcmpsurinjALT  44864  sprbisymrel  44951  uspgrbisymrelALT  45317  funcrngcsetc  45556  funcringcsetc  45593  scmsuppss  45708  rmfsupp  45710  scmfsupp  45714  mptcfsupp  45716  lincresunit2  45819  itcoval0mpt  46012  eufsn  46169