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 6606	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2735	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6263	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5329	. . 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 2106  Vcvv 3478   ⊆ wss 3963   ↦ cmpt 5231  dom cdm 5689  Fun wfun 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571

This theorem is referenced by:  mptex  7243  mptexd  7244  ovmpt3rab1  7691  offval  7706  abrexexgOLD  7985  xpexgALT  8005  offval3  8006  suppssov1  8221  suppssov2  8222  suppssfv  8226  iunon  8378  onoviun  8382  mptelixpg  8974  cantnfp1lem1  9716  updjud  9972  coftr  10311  axcc3  10476  reps  14805  wrd2f1tovbij  14996  restval  17473  resf1st  17945  resf2nd  17946  funcres  17947  vrmdfval  18882  symgfixfolem1  19471  pmtrval  19484  pmtrrn  19490  pmtrfrn  19491  sylow1lem4  19634  sylow3lem2  19661  sylow3lem3  19662  funcrngcsetc  20657  funcringcsetc  20691  uvcfval  21822  uvcval  21823  uvcff  21829  uvcresum  21831  psrass1lem  21970  opsrval  22082  selvfval  22156  psropprmul  22255  mavmuldm  22572  mat2pmatfval  22745  cpm2mfval  22771  chpmatfval  22852  ntrfval  23048  clsfval  23049  neifval  23123  lpfval  23162  ptcnplem  23645  upxp  23647  fmfnfmlem3  23980  fmfnfmlem4  23981  ustuqtoplem  24264  ustuqtop0  24265  utopsnneiplem  24272  rrxmval  25453  tayl0  26418  itgulm2  26467  efabl  26607  tgjustr  28497  lmif  28808  islmib  28810  nbusgrf1o1  29402  cusgrfilem3  29490  vtxdgfval  29500  wlkiswwlks2  29905  wwlksnextbij  29932  clwlkclwwlklem1  30028  grpoinvfval  30551  acunirnmpt  32676  acunirnmpt2  32677  acunirnmpt2f  32678  aciunf1lem  32679  fnpreimac  32688  mptiffisupp  32708  frlmdim  33639  indv  33993  indval  33994  ofcfval3  34083  omsval  34275  carsgclctunlem2  34301  pmeasadd  34307  sitgclg  34324  bnj1366  34822  ptpconn  35218  fwddifval  36144  tailfval  36355  curfv  37587  matunitlindflem1  37603  matunitlindflem2  37604  upixp  37716  pw2f1ocnv  43026  kelac1  43052  rfovd  43991  fsovrfovd  43999  dssmapfvd  44007  dssmapfv2d  44008  fmulcl  45537  fmuldfeqlem1  45538  dvnmul  45899  dvnprodlem2  45903  stoweidlem31  45987  stoweidlem42  45998  stoweidlem48  46004  etransclem1  46191  etransclem4  46194  etransclem13  46203  etransclem17  46207  0ome  46485  hoicvr  46504  hsphoif  46532  hsphoival  46535  hoidmvlelem2  46552  hoidmvlelem3  46553  ovnhoilem1  46557  ovnhoilem2  46558  ovnlecvr2  46566  ovncvr2  46567  hoidifhspval2  46571  hspmbllem2  46583  fundcmpsurinjALT  47337  sprbisymrel  47424  uspgrbisymrelALT  47999  scmsuppss  48216  rmfsupp  48218  scmfsupp  48220  mptcfsupp  48222  lincresunit2  48324  itcoval0mpt  48516  eufsn  48672