Theorem mptexg 7195

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914   ↦ cmpt 5188  dom cdm 5638  Fun wfun 6505

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519

This theorem is referenced by:  mptex  7197  mptexd  7198  ovmpt3rab1  7647  offval  7662  abrexexgOLD  7940  xpexgALT  7960  offval3  7961  suppssov1  8176  suppssov2  8177  suppssfv  8181  iunon  8308  onoviun  8312  mptelixpg  8908  cantnfp1lem1  9631  updjud  9887  coftr  10226  axcc3  10391  reps  14735  wrd2f1tovbij  14926  restval  17389  resf1st  17856  resf2nd  17857  funcres  17858  vrmdfval  18783  symgfixfolem1  19368  pmtrval  19381  pmtrrn  19387  pmtrfrn  19388  sylow1lem4  19531  sylow3lem2  19558  sylow3lem3  19559  funcrngcsetc  20549  funcringcsetc  20583  uvcfval  21693  uvcval  21694  uvcff  21700  uvcresum  21702  psrass1lem  21841  opsrval  21953  selvfval  22021  psropprmul  22122  mavmuldm  22437  mat2pmatfval  22610  cpm2mfval  22636  chpmatfval  22717  ntrfval  22911  clsfval  22912  neifval  22986  lpfval  23025  ptcnplem  23508  upxp  23510  fmfnfmlem3  23843  fmfnfmlem4  23844  ustuqtoplem  24127  ustuqtop0  24128  utopsnneiplem  24135  rrxmval  25305  tayl0  26269  itgulm2  26318  efabl  26459  tgjustr  28401  lmif  28712  islmib  28714  nbusgrf1o1  29297  cusgrfilem3  29385  vtxdgfval  29395  wlkiswwlks2  29805  wwlksnextbij  29832  clwlkclwwlklem1  29928  grpoinvfval  30451  acunirnmpt  32583  acunirnmpt2  32584  acunirnmpt2f  32585  aciunf1lem  32586  fnpreimac  32595  mptiffisupp  32616  indv  32775  indval  32776  frlmdim  33607  ofcfval3  34092  omsval  34284  carsgclctunlem2  34310  pmeasadd  34316  sitgclg  34333  bnj1366  34819  ptpconn  35220  fwddifval  36150  tailfval  36360  curfv  37594  matunitlindflem1  37610  matunitlindflem2  37611  upixp  37723  pw2f1ocnv  43026  kelac1  43052  rfovd  43990  fsovrfovd  43998  dssmapfvd  44006  dssmapfv2d  44007  fmulcl  45579  fmuldfeqlem1  45580  dvnmul  45941  dvnprodlem2  45945  stoweidlem31  46029  stoweidlem42  46040  stoweidlem48  46046  etransclem1  46233  etransclem4  46236  etransclem13  46245  etransclem17  46249  0ome  46527  hoicvr  46546  hsphoif  46574  hsphoival  46577  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem1  46599  ovnhoilem2  46600  ovnlecvr2  46608  ovncvr2  46609  hoidifhspval2  46613  hspmbllem2  46625  fundcmpsurinjALT  47413  sprbisymrel  47500  uspgrbisymrelALT  48143  scmsuppss  48359  rmfsupp  48361  scmfsupp  48363  mptcfsupp  48365  lincresunit2  48467  itcoval0mpt  48655  eufsn  48830