Theorem mptexg 7169

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890   ↦ cmpt 5167  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 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 5212  ax-sep 5231  ax-nul 5241  ax-pr 5370

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 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  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  7171  mptexd  7172  ovmpt3rab1  7618  offval  7633  xpexgALT  7927  offval3  7928  suppssov1  8140  suppssov2  8141  suppssfv  8145  iunon  8272  onoviun  8276  mptelixpg  8876  cantnfp1lem1  9590  updjud  9849  coftr  10186  axcc3  10351  indv  12152  indval  12153  reps  14723  wrd2f1tovbij  14913  restval  17380  resf1st  17852  resf2nd  17853  funcres  17854  vrmdfval  18815  symgfixfolem1  19404  pmtrval  19417  pmtrrn  19423  pmtrfrn  19424  sylow1lem4  19567  sylow3lem2  19594  sylow3lem3  19595  funcrngcsetc  20608  funcringcsetc  20642  uvcfval  21774  uvcval  21775  uvcff  21781  uvcresum  21783  psrass1lem  21922  opsrval  22034  selvfval  22110  psropprmul  22211  mavmuldm  22525  mat2pmatfval  22698  cpm2mfval  22724  chpmatfval  22805  ntrfval  22999  clsfval  23000  neifval  23074  lpfval  23113  ptcnplem  23596  upxp  23598  fmfnfmlem3  23931  fmfnfmlem4  23932  ustuqtoplem  24214  ustuqtop0  24215  utopsnneiplem  24222  rrxmval  25382  tayl0  26338  itgulm2  26387  efabl  26527  tgjustr  28556  lmif  28867  islmib  28869  nbusgrf1o1  29453  cusgrfilem3  29541  vtxdgfval  29551  wlkiswwlks2  29958  wwlksnextbij  29985  clwlkclwwlklem1  30084  grpoinvfval  30608  acunirnmpt  32747  acunirnmpt2  32748  acunirnmpt2f  32749  aciunf1lem  32750  fnpreimac  32758  mptiffisupp  32781  frlmdim  33771  ofcfval3  34262  omsval  34453  carsgclctunlem2  34479  pmeasadd  34485  sitgclg  34502  bnj1366  34987  ptpconn  35431  fwddifval  36360  tailfval  36570  curfv  37935  matunitlindflem1  37951  matunitlindflem2  37952  upixp  38064  pw2f1ocnv  43483  kelac1  43509  rfovd  44446  fsovrfovd  44454  dssmapfvd  44462  dssmapfv2d  44463  fmulcl  46029  fmuldfeqlem1  46030  dvnmul  46389  dvnprodlem2  46393  stoweidlem31  46477  stoweidlem42  46488  stoweidlem48  46494  etransclem1  46681  etransclem4  46684  etransclem13  46693  etransclem17  46697  0ome  46975  hsphoif  47022  hsphoival  47025  hoidmvlelem2  47042  hoidmvlelem3  47043  ovnhoilem1  47047  ovnhoilem2  47048  ovnlecvr2  47056  ovncvr2  47057  hoidifhspval2  47061  hspmbllem2  47073  fundcmpsurinjALT  47884  sprbisymrel  47971  uspgrbisymrelALT  48643  scmsuppss  48859  rmfsupp  48861  scmfsupp  48863  mptcfsupp  48865  lincresunit2  48966  itcoval0mpt  49154  eufsn  49329