Theorem mptexg 7161

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3437   ⊆ wss 3898   ↦ cmpt 5174  dom cdm 5619  Fun wfun 6480

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 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pr 5372

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494

This theorem is referenced by:  mptex  7163  mptexd  7164  ovmpt3rab1  7610  offval  7625  xpexgALT  7919  offval3  7920  suppssov1  8133  suppssov2  8134  suppssfv  8138  iunon  8265  onoviun  8269  mptelixpg  8865  cantnfp1lem1  9575  updjud  9834  coftr  10171  axcc3  10336  reps  14679  wrd2f1tovbij  14869  restval  17332  resf1st  17803  resf2nd  17804  funcres  17805  vrmdfval  18766  symgfixfolem1  19352  pmtrval  19365  pmtrrn  19371  pmtrfrn  19372  sylow1lem4  19515  sylow3lem2  19542  sylow3lem3  19543  funcrngcsetc  20557  funcringcsetc  20591  uvcfval  21723  uvcval  21724  uvcff  21730  uvcresum  21732  psrass1lem  21871  opsrval  21982  selvfval  22050  psropprmul  22151  mavmuldm  22466  mat2pmatfval  22639  cpm2mfval  22665  chpmatfval  22746  ntrfval  22940  clsfval  22941  neifval  23015  lpfval  23054  ptcnplem  23537  upxp  23539  fmfnfmlem3  23872  fmfnfmlem4  23873  ustuqtoplem  24155  ustuqtop0  24156  utopsnneiplem  24163  rrxmval  25333  tayl0  26297  itgulm2  26346  efabl  26487  tgjustr  28453  lmif  28764  islmib  28766  nbusgrf1o1  29350  cusgrfilem3  29438  vtxdgfval  29448  wlkiswwlks2  29855  wwlksnextbij  29882  clwlkclwwlklem1  29981  grpoinvfval  30504  acunirnmpt  32643  acunirnmpt2  32644  acunirnmpt2f  32645  aciunf1lem  32646  fnpreimac  32655  mptiffisupp  32678  indv  32838  indval  32839  frlmdim  33645  ofcfval3  34136  omsval  34327  carsgclctunlem2  34353  pmeasadd  34359  sitgclg  34376  bnj1366  34862  ptpconn  35298  fwddifval  36227  tailfval  36437  curfv  37660  matunitlindflem1  37676  matunitlindflem2  37677  upixp  37789  pw2f1ocnv  43154  kelac1  43180  rfovd  44118  fsovrfovd  44126  dssmapfvd  44134  dssmapfv2d  44135  fmulcl  45705  fmuldfeqlem1  45706  dvnmul  46065  dvnprodlem2  46069  stoweidlem31  46153  stoweidlem42  46164  stoweidlem48  46170  etransclem1  46357  etransclem4  46360  etransclem13  46369  etransclem17  46373  0ome  46651  hoicvr  46670  hsphoif  46698  hsphoival  46701  hoidmvlelem2  46718  hoidmvlelem3  46719  ovnhoilem1  46723  ovnhoilem2  46724  ovnlecvr2  46732  ovncvr2  46733  hoidifhspval2  46737  hspmbllem2  46749  fundcmpsurinjALT  47536  sprbisymrel  47623  uspgrbisymrelALT  48279  scmsuppss  48495  rmfsupp  48497  scmfsupp  48499  mptcfsupp  48501  lincresunit2  48603  itcoval0mpt  48791  eufsn  48966