Theorem mptexg 7167

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 6530	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2736	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6199	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5268	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 690	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 7165	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 587	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901   ↦ cmpt 5179  dom cdm 5624  Fun wfun 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  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:  mptex  7169  mptexd  7170  ovmpt3rab1  7616  offval  7631  xpexgALT  7925  offval3  7926  suppssov1  8139  suppssov2  8140  suppssfv  8144  iunon  8271  onoviun  8275  mptelixpg  8873  cantnfp1lem1  9587  updjud  9846  coftr  10183  axcc3  10348  reps  14693  wrd2f1tovbij  14883  restval  17346  resf1st  17818  resf2nd  17819  funcres  17820  vrmdfval  18781  symgfixfolem1  19367  pmtrval  19380  pmtrrn  19386  pmtrfrn  19387  sylow1lem4  19530  sylow3lem2  19557  sylow3lem3  19558  funcrngcsetc  20573  funcringcsetc  20607  uvcfval  21739  uvcval  21740  uvcff  21746  uvcresum  21748  psrass1lem  21888  opsrval  22001  selvfval  22077  psropprmul  22178  mavmuldm  22494  mat2pmatfval  22667  cpm2mfval  22693  chpmatfval  22774  ntrfval  22968  clsfval  22969  neifval  23043  lpfval  23082  ptcnplem  23565  upxp  23567  fmfnfmlem3  23900  fmfnfmlem4  23901  ustuqtoplem  24183  ustuqtop0  24184  utopsnneiplem  24191  rrxmval  25361  tayl0  26325  itgulm2  26374  efabl  26515  tgjustr  28546  lmif  28857  islmib  28859  nbusgrf1o1  29443  cusgrfilem3  29531  vtxdgfval  29541  wlkiswwlks2  29948  wwlksnextbij  29975  clwlkclwwlklem1  30074  grpoinvfval  30597  acunirnmpt  32737  acunirnmpt2  32738  acunirnmpt2f  32739  aciunf1lem  32740  fnpreimac  32749  mptiffisupp  32772  indv  32931  indval  32932  frlmdim  33768  ofcfval3  34259  omsval  34450  carsgclctunlem2  34476  pmeasadd  34482  sitgclg  34499  bnj1366  34985  ptpconn  35427  fwddifval  36356  tailfval  36566  curfv  37797  matunitlindflem1  37813  matunitlindflem2  37814  upixp  37926  pw2f1ocnv  43275  kelac1  43301  rfovd  44238  fsovrfovd  44246  dssmapfvd  44254  dssmapfv2d  44255  fmulcl  45823  fmuldfeqlem1  45824  dvnmul  46183  dvnprodlem2  46187  stoweidlem31  46271  stoweidlem42  46282  stoweidlem48  46288  etransclem1  46475  etransclem4  46478  etransclem13  46487  etransclem17  46491  0ome  46769  hoicvr  46788  hsphoif  46816  hsphoival  46819  hoidmvlelem2  46836  hoidmvlelem3  46837  ovnhoilem1  46841  ovnhoilem2  46842  ovnlecvr2  46850  ovncvr2  46851  hoidifhspval2  46855  hspmbllem2  46867  fundcmpsurinjALT  47654  sprbisymrel  47741  uspgrbisymrelALT  48397  scmsuppss  48613  rmfsupp  48615  scmfsupp  48617  mptcfsupp  48619  lincresunit2  48720  itcoval0mpt  48908  eufsn  49083