Theorem mptexg 7172

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 2740	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6199	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5258	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 696	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 7170	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 593	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3432   ⊆ wss 3890   ↦ cmpt 5160  dom cdm 5625  Fun wfun 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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  7174  mptexd  7175  ovmpt3rab1  7621  offval  7636  xpexgALT  7930  offval3  7931  suppssov1  8144  suppssov2  8145  suppssfv  8149  iunon  8276  onoviun  8280  mptelixpg  8880  cantnfp1lem1  9597  updjud  9856  coftr  10193  axcc3  10358  indv  12159  indval  12160  reps  14730  wrd2f1tovbij  14920  restval  17387  resf1st  17859  resf2nd  17860  funcres  17861  vrmdfval  18822  symgfixfolem1  19411  pmtrval  19424  pmtrrn  19430  pmtrfrn  19431  sylow1lem4  19574  sylow3lem2  19601  sylow3lem3  19602  funcrngcsetc  20619  funcringcsetc  20653  uvcfval  21766  uvcval  21767  uvcff  21773  uvcresum  21775  psrass1lem  21915  opsrval  22029  selvfval  22102  psropprmul  22229  mavmuldm  22540  mat2pmatfval  22713  cpm2mfval  22739  chpmatfval  22820  ntrfval  23014  clsfval  23015  neifval  23089  lpfval  23128  ptcnplem  23611  upxp  23613  fmfnfmlem3  23946  fmfnfmlem4  23947  ustuqtoplem  24229  ustuqtop0  24230  utopsnneiplem  24237  rrxmval  25397  tayl0  26352  itgulm2  26399  efabl  26539  tgjustr  28567  lmif  28878  islmib  28880  nbusgrf1o1  29464  cusgrfilem3  29551  vtxdgfval  29561  wlkiswwlks2  29968  wwlksnextbij  29995  clwlkclwwlklem1  30094  grpoinvfval  30618  acunirnmpt  32758  acunirnmpt2  32759  acunirnmpt2f  32760  aciunf1lem  32761  fnpreimac  32769  mptiffisupp  32792  frlmdim  33802  ofcfval3  34293  omsval  34484  carsgclctunlem2  34510  pmeasadd  34516  sitgclg  34533  bnj1366  35018  ptpconn  35468  fwddifval  36397  tailfval  36607  curfv  37974  matunitlindflem1  37990  matunitlindflem2  37991  upixp  38103  pw2f1ocnv  43489  kelac1  43515  rfovd  44452  fsovrfovd  44460  dssmapfvd  44468  dssmapfv2d  44469  fmulcl  46033  fmuldfeqlem1  46034  dvnmul  46393  dvnprodlem2  46397  stoweidlem31  46481  stoweidlem42  46492  stoweidlem48  46498  etransclem1  46685  etransclem4  46688  etransclem13  46697  etransclem17  46701  0ome  46979  hsphoif  47026  hsphoival  47029  hoidmvlelem2  47046  hoidmvlelem3  47047  ovnhoilem1  47051  ovnhoilem2  47052  ovnlecvr2  47060  ovncvr2  47061  hoidifhspval2  47065  hspmbllem2  47077  fundcmpsurinjALT  47894  sprbisymrel  47981  uspgrbisymrelALT  48653  scmsuppss  48869  rmfsupp  48871  scmfsupp  48873  mptcfsupp  48875  lincresunit2  48976  itcoval0mpt  49164  eufsn  49339