Theorem mptexg 6804

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 6220	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2772	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 5928	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5077	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 677	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 6802	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 578	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2048  Vcvv 3409   ⊆ wss 3825   ↦ cmpt 5002  dom cdm 5400  Fun wfun 6176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pr 5180

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5305  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190

This theorem is referenced by:  mptex  6806  mptexd  6807  ovmpt3rab1  7215  offval  7228  abrexexg  7468  xpexgALT  7487  offval3  7488  suppssov1  7658  suppssfv  7662  iunon  7773  onoviun  7777  mptelixpg  8288  cantnfp1lem1  8927  updjud  9149  coftr  9485  axcc3  9650  reps  13979  wrd2f1tovbij  14175  restval  16546  resf1st  17012  resf2nd  17013  funcres  17014  vrmdfval  17852  symgfixfolem1  18317  pmtrval  18330  pmtrrn  18336  pmtrfrn  18337  sylow1lem4  18477  sylow3lem2  18504  sylow3lem3  18505  psrass1lem  19861  opsrval  19958  psropprmul  20099  uvcfval  20620  uvcval  20621  uvcff  20627  uvcresum  20629  mavmuldm  20853  mat2pmatfval  21025  cpm2mfval  21051  chpmatfval  21132  ntrfval  21326  clsfval  21327  neifval  21401  lpfval  21440  ptcnplem  21923  upxp  21925  fmfnfmlem3  22258  fmfnfmlem4  22259  ustuqtoplem  22541  ustuqtop0  22542  utopsnneiplem  22549  rrxmval  23701  tdeglem4  24347  tayl0  24643  itgulm2  24690  efabl  24825  tgjustr  25952  lmif  26263  islmib  26265  nbusgrf1o1  26845  cusgrfilem3  26932  vtxdgfval  26942  wlkiswwlks2  27351  wwlksnextbij  27388  wwlksnextbijOLD  27389  clwlkclwwlklem1  27495  grpoinvfval  28066  acunirnmpt  30156  acunirnmpt2  30157  acunirnmpt2f  30158  aciunf1lem  30159  fnpreimac  30168  frlmdim  30594  indv  30872  indval  30873  ofcfval3  30962  omsval  31153  carsgclctunlem2  31179  pmeasadd  31185  sitgclg  31202  bnj1366  31710  ptpconn  32025  fwddifval  33084  tailfval  33181  curfv  34261  matunitlindflem1  34277  matunitlindflem2  34278  upixp  34394  pw2f1ocnv  38975  kelac1  39004  rfovd  39655  rfovfvd  39656  fsovrfovd  39663  dssmapfvd  39671  dssmapfv2d  39672  dssmapf1od  39675  fmulcl  41239  fmuldfeqlem1  41240  dvnmul  41604  dvnprodlem2  41608  stoweidlem31  41693  stoweidlem42  41704  stoweidlem48  41710  etransclem1  41897  etransclem4  41900  etransclem13  41909  etransclem17  41913  0ome  42188  hoicvr  42207  hsphoif  42235  hsphoival  42238  hoidmvlelem2  42255  hoidmvlelem3  42256  ovnhoilem1  42260  ovnhoilem2  42261  ovnlecvr2  42269  ovncvr2  42270  hoidifhspval2  42274  hspmbllem2  42286  sprbisymrel  42969  uspgrbisymrelALT  43338  funcrngcsetc  43573  funcringcsetc  43610  scmsuppss  43726  rmfsupp  43728  scmfsupp  43732  mptcfsupp  43734  lincresunit2  43840  offval0  43872