Theorem mptexg 7241

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951   ↦ cmpt 5225  dom cdm 5685  Fun wfun 6555

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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569

This theorem is referenced by:  mptex  7243  mptexd  7244  ovmpt3rab1  7691  offval  7706  abrexexgOLD  7986  xpexgALT  8006  offval3  8007  suppssov1  8222  suppssov2  8223  suppssfv  8227  iunon  8379  onoviun  8383  mptelixpg  8975  cantnfp1lem1  9718  updjud  9974  coftr  10313  axcc3  10478  reps  14808  wrd2f1tovbij  14999  restval  17471  resf1st  17939  resf2nd  17940  funcres  17941  vrmdfval  18869  symgfixfolem1  19456  pmtrval  19469  pmtrrn  19475  pmtrfrn  19476  sylow1lem4  19619  sylow3lem2  19646  sylow3lem3  19647  funcrngcsetc  20640  funcringcsetc  20674  uvcfval  21804  uvcval  21805  uvcff  21811  uvcresum  21813  psrass1lem  21952  opsrval  22064  selvfval  22138  psropprmul  22239  mavmuldm  22556  mat2pmatfval  22729  cpm2mfval  22755  chpmatfval  22836  ntrfval  23032  clsfval  23033  neifval  23107  lpfval  23146  ptcnplem  23629  upxp  23631  fmfnfmlem3  23964  fmfnfmlem4  23965  ustuqtoplem  24248  ustuqtop0  24249  utopsnneiplem  24256  rrxmval  25439  tayl0  26403  itgulm2  26452  efabl  26592  tgjustr  28482  lmif  28793  islmib  28795  nbusgrf1o1  29387  cusgrfilem3  29475  vtxdgfval  29485  wlkiswwlks2  29895  wwlksnextbij  29922  clwlkclwwlklem1  30018  grpoinvfval  30541  acunirnmpt  32669  acunirnmpt2  32670  acunirnmpt2f  32671  aciunf1lem  32672  fnpreimac  32681  mptiffisupp  32702  indv  32837  indval  32838  frlmdim  33662  ofcfval3  34103  omsval  34295  carsgclctunlem2  34321  pmeasadd  34327  sitgclg  34344  bnj1366  34843  ptpconn  35238  fwddifval  36163  tailfval  36373  curfv  37607  matunitlindflem1  37623  matunitlindflem2  37624  upixp  37736  pw2f1ocnv  43049  kelac1  43075  rfovd  44014  fsovrfovd  44022  dssmapfvd  44030  dssmapfv2d  44031  fmulcl  45596  fmuldfeqlem1  45597  dvnmul  45958  dvnprodlem2  45962  stoweidlem31  46046  stoweidlem42  46057  stoweidlem48  46063  etransclem1  46250  etransclem4  46253  etransclem13  46262  etransclem17  46266  0ome  46544  hoicvr  46563  hsphoif  46591  hsphoival  46594  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoilem1  46616  ovnhoilem2  46617  ovnlecvr2  46625  ovncvr2  46626  hoidifhspval2  46630  hspmbllem2  46642  fundcmpsurinjALT  47399  sprbisymrel  47486  uspgrbisymrelALT  48071  scmsuppss  48287  rmfsupp  48289  scmfsupp  48291  mptcfsupp  48293  lincresunit2  48395  itcoval0mpt  48587  eufsn  48751