Theorem mptexg 6978

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 6387	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2821	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6089	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5219	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 688	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 6976	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 589	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3494   ⊆ wss 3935   ↦ cmpt 5138  dom cdm 5549  Fun wfun 6343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357

This theorem is referenced by:  mptex  6980  mptexd  6981  ovmpt3rab1  7397  offval  7410  abrexexg  7656  xpexgALT  7676  offval3  7677  suppssov1  7856  suppssfv  7860  iunon  7970  onoviun  7974  mptelixpg  8493  cantnfp1lem1  9135  updjud  9357  coftr  9689  axcc3  9854  reps  14126  wrd2f1tovbij  14318  restval  16694  resf1st  17158  resf2nd  17159  funcres  17160  vrmdfval  18015  symgfixfolem1  18560  pmtrval  18573  pmtrrn  18579  pmtrfrn  18580  sylow1lem4  18720  sylow3lem2  18747  sylow3lem3  18748  psrass1lem  20151  opsrval  20249  selvfval  20324  psropprmul  20400  uvcfval  20922  uvcval  20923  uvcff  20929  uvcresum  20931  mavmuldm  21153  mat2pmatfval  21325  cpm2mfval  21351  chpmatfval  21432  ntrfval  21626  clsfval  21627  neifval  21701  lpfval  21740  ptcnplem  22223  upxp  22225  fmfnfmlem3  22558  fmfnfmlem4  22559  ustuqtoplem  22842  ustuqtop0  22843  utopsnneiplem  22850  rrxmval  24002  tdeglem4  24648  tayl0  24944  itgulm2  24991  efabl  25128  tgjustr  26254  lmif  26565  islmib  26567  nbusgrf1o1  27146  cusgrfilem3  27233  vtxdgfval  27243  wlkiswwlks2  27647  wwlksnextbij  27674  clwlkclwwlklem1  27771  grpoinvfval  28293  acunirnmpt  30398  acunirnmpt2  30399  acunirnmpt2f  30400  aciunf1lem  30401  fnpreimac  30410  frlmdim  31004  indv  31266  indval  31267  ofcfval3  31356  omsval  31546  carsgclctunlem2  31572  pmeasadd  31578  sitgclg  31595  bnj1366  32096  ptpconn  32475  fwddifval  33618  tailfval  33715  curfv  34866  matunitlindflem1  34882  matunitlindflem2  34883  upixp  34998  pw2f1ocnv  39627  kelac1  39656  rfovd  40340  fsovrfovd  40348  dssmapfvd  40356  dssmapfv2d  40357  fmulcl  41855  fmuldfeqlem1  41856  dvnmul  42221  dvnprodlem2  42225  stoweidlem31  42310  stoweidlem42  42321  stoweidlem48  42327  etransclem1  42514  etransclem4  42517  etransclem13  42526  etransclem17  42530  0ome  42805  hoicvr  42824  hsphoif  42852  hsphoival  42855  hoidmvlelem2  42872  hoidmvlelem3  42873  ovnhoilem1  42877  ovnhoilem2  42878  ovnlecvr2  42886  ovncvr2  42887  hoidifhspval2  42891  hspmbllem2  42903  fundcmpsurinjALT  43566  sprbisymrel  43655  uspgrbisymrelALT  44024  funcrngcsetc  44263  funcringcsetc  44300  scmsuppss  44414  rmfsupp  44416  scmfsupp  44420  mptcfsupp  44422  lincresunit2  44527