Theorem mptexg 7176

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 6536	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2736	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6205	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5264	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 691	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 7174	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 588	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889   ↦ cmpt 5166  dom cdm 5631  Fun wfun 6492

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 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506

This theorem is referenced by:  mptex  7178  mptexd  7179  ovmpt3rab1  7625  offval  7640  xpexgALT  7934  offval3  7935  suppssov1  8147  suppssov2  8148  suppssfv  8152  iunon  8279  onoviun  8283  mptelixpg  8883  cantnfp1lem1  9599  updjud  9858  coftr  10195  axcc3  10360  indv  12161  indval  12162  reps  14732  wrd2f1tovbij  14922  restval  17389  resf1st  17861  resf2nd  17862  funcres  17863  vrmdfval  18824  symgfixfolem1  19413  pmtrval  19426  pmtrrn  19432  pmtrfrn  19433  sylow1lem4  19576  sylow3lem2  19603  sylow3lem3  19604  funcrngcsetc  20617  funcringcsetc  20651  uvcfval  21764  uvcval  21765  uvcff  21771  uvcresum  21773  psrass1lem  21912  opsrval  22024  selvfval  22100  psropprmul  22201  mavmuldm  22515  mat2pmatfval  22688  cpm2mfval  22714  chpmatfval  22795  ntrfval  22989  clsfval  22990  neifval  23064  lpfval  23103  ptcnplem  23586  upxp  23588  fmfnfmlem3  23921  fmfnfmlem4  23922  ustuqtoplem  24204  ustuqtop0  24205  utopsnneiplem  24212  rrxmval  25372  tayl0  26327  itgulm2  26374  efabl  26514  tgjustr  28542  lmif  28853  islmib  28855  nbusgrf1o1  29439  cusgrfilem3  29526  vtxdgfval  29536  wlkiswwlks2  29943  wwlksnextbij  29970  clwlkclwwlklem1  30069  grpoinvfval  30593  acunirnmpt  32732  acunirnmpt2  32733  acunirnmpt2f  32734  aciunf1lem  32735  fnpreimac  32743  mptiffisupp  32766  frlmdim  33755  ofcfval3  34246  omsval  34437  carsgclctunlem2  34463  pmeasadd  34469  sitgclg  34486  bnj1366  34971  ptpconn  35415  fwddifval  36344  tailfval  36554  curfv  37921  matunitlindflem1  37937  matunitlindflem2  37938  upixp  38050  pw2f1ocnv  43465  kelac1  43491  rfovd  44428  fsovrfovd  44436  dssmapfvd  44444  dssmapfv2d  44445  fmulcl  46011  fmuldfeqlem1  46012  dvnmul  46371  dvnprodlem2  46375  stoweidlem31  46459  stoweidlem42  46470  stoweidlem48  46476  etransclem1  46663  etransclem4  46666  etransclem13  46675  etransclem17  46679  0ome  46957  hsphoif  47004  hsphoival  47007  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem1  47029  ovnhoilem2  47030  ovnlecvr2  47038  ovncvr2  47039  hoidifhspval2  47043  hspmbllem2  47055  fundcmpsurinjALT  47872  sprbisymrel  47959  uspgrbisymrelALT  48631  scmsuppss  48847  rmfsupp  48849  scmfsupp  48851  mptcfsupp  48853  lincresunit2  48954  itcoval0mpt  49142  eufsn  49317