Theorem mptexg 6987

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3497   ⊆ wss 3939   ↦ cmpt 5149  dom cdm 5558  Fun wfun 6352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pr 5333

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366

This theorem is referenced by:  mptex  6989  mptexd  6990  ovmpt3rab1  7406  offval  7419  abrexexg  7665  xpexgALT  7685  offval3  7686  suppssov1  7865  suppssfv  7869  iunon  7979  onoviun  7983  mptelixpg  8502  cantnfp1lem1  9144  updjud  9366  coftr  9698  axcc3  9863  reps  14135  wrd2f1tovbij  14327  restval  16703  resf1st  17167  resf2nd  17168  funcres  17169  vrmdfval  18024  symgfixfolem1  18569  pmtrval  18582  pmtrrn  18588  pmtrfrn  18589  sylow1lem4  18729  sylow3lem2  18756  sylow3lem3  18757  psrass1lem  20160  opsrval  20258  selvfval  20333  psropprmul  20409  uvcfval  20931  uvcval  20932  uvcff  20938  uvcresum  20940  mavmuldm  21162  mat2pmatfval  21334  cpm2mfval  21360  chpmatfval  21441  ntrfval  21635  clsfval  21636  neifval  21710  lpfval  21749  ptcnplem  22232  upxp  22234  fmfnfmlem3  22567  fmfnfmlem4  22568  ustuqtoplem  22851  ustuqtop0  22852  utopsnneiplem  22859  rrxmval  24011  tdeglem4  24657  tayl0  24953  itgulm2  25000  efabl  25137  tgjustr  26263  lmif  26574  islmib  26576  nbusgrf1o1  27155  cusgrfilem3  27242  vtxdgfval  27252  wlkiswwlks2  27656  wwlksnextbij  27683  clwlkclwwlklem1  27780  grpoinvfval  28302  acunirnmpt  30407  acunirnmpt2  30408  acunirnmpt2f  30409  aciunf1lem  30410  fnpreimac  30419  frlmdim  31013  indv  31275  indval  31276  ofcfval3  31365  omsval  31555  carsgclctunlem2  31581  pmeasadd  31587  sitgclg  31604  bnj1366  32105  ptpconn  32484  fwddifval  33627  tailfval  33724  curfv  34876  matunitlindflem1  34892  matunitlindflem2  34893  upixp  35008  pw2f1ocnv  39640  kelac1  39669  rfovd  40353  fsovrfovd  40361  dssmapfvd  40369  dssmapfv2d  40370  fmulcl  41868  fmuldfeqlem1  41869  dvnmul  42234  dvnprodlem2  42238  stoweidlem31  42323  stoweidlem42  42334  stoweidlem48  42340  etransclem1  42527  etransclem4  42530  etransclem13  42539  etransclem17  42543  0ome  42818  hoicvr  42837  hsphoif  42865  hsphoival  42868  hoidmvlelem2  42885  hoidmvlelem3  42886  ovnhoilem1  42890  ovnhoilem2  42891  ovnlecvr2  42899  ovncvr2  42900  hoidifhspval2  42904  hspmbllem2  42916  fundcmpsurinjALT  43579  sprbisymrel  43668  uspgrbisymrelALT  44037  funcrngcsetc  44276  funcringcsetc  44313  scmsuppss  44427  rmfsupp  44429  scmfsupp  44433  mptcfsupp  44435  lincresunit2  44540