Theorem mptexg 7222

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474   ⊆ wss 3948   ↦ cmpt 5231  dom cdm 5676  Fun wfun 6537

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551

This theorem is referenced by:  mptex  7224  mptexd  7225  ovmpt3rab1  7663  offval  7678  abrexexgOLD  7947  xpexgALT  7967  offval3  7968  suppssov1  8182  suppssfv  8186  iunon  8338  onoviun  8342  mptelixpg  8928  cantnfp1lem1  9672  updjud  9928  coftr  10267  axcc3  10432  reps  14719  wrd2f1tovbij  14910  restval  17371  resf1st  17843  resf2nd  17844  funcres  17845  vrmdfval  18736  symgfixfolem1  19305  pmtrval  19318  pmtrrn  19324  pmtrfrn  19325  sylow1lem4  19468  sylow3lem2  19495  sylow3lem3  19496  uvcfval  21338  uvcval  21339  uvcff  21345  uvcresum  21347  psrass1lemOLD  21492  psrass1lem  21495  opsrval  21600  selvfval  21679  psropprmul  21759  mavmuldm  22051  mat2pmatfval  22224  cpm2mfval  22250  chpmatfval  22331  ntrfval  22527  clsfval  22528  neifval  22602  lpfval  22641  ptcnplem  23124  upxp  23126  fmfnfmlem3  23459  fmfnfmlem4  23460  ustuqtoplem  23743  ustuqtop0  23744  utopsnneiplem  23751  rrxmval  24921  tdeglem4OLD  25577  tayl0  25873  itgulm2  25920  efabl  26058  tgjustr  27722  lmif  28033  islmib  28035  nbusgrf1o1  28624  cusgrfilem3  28711  vtxdgfval  28721  wlkiswwlks2  29126  wwlksnextbij  29153  clwlkclwwlklem1  29249  grpoinvfval  29770  acunirnmpt  31879  acunirnmpt2  31880  acunirnmpt2f  31881  aciunf1lem  31882  fnpreimac  31891  mptiffisupp  31910  frlmdim  32691  indv  33005  indval  33006  ofcfval3  33095  omsval  33287  carsgclctunlem2  33313  pmeasadd  33319  sitgclg  33336  bnj1366  33835  ptpconn  34219  fwddifval  35129  tailfval  35252  curfv  36463  matunitlindflem1  36479  matunitlindflem2  36480  upixp  36592  pw2f1ocnv  41766  kelac1  41795  rfovd  42742  fsovrfovd  42750  dssmapfvd  42758  dssmapfv2d  42759  fmulcl  44287  fmuldfeqlem1  44288  dvnmul  44649  dvnprodlem2  44653  stoweidlem31  44737  stoweidlem42  44748  stoweidlem48  44754  etransclem1  44941  etransclem4  44944  etransclem13  44953  etransclem17  44957  0ome  45235  hoicvr  45254  hsphoif  45282  hsphoival  45285  hoidmvlelem2  45302  hoidmvlelem3  45303  ovnhoilem1  45307  ovnhoilem2  45308  ovnlecvr2  45316  ovncvr2  45317  hoidifhspval2  45321  hspmbllem2  45333  fundcmpsurinjALT  46070  sprbisymrel  46157  uspgrbisymrelALT  46523  funcrngcsetc  46886  funcringcsetc  46923  scmsuppss  47038  rmfsupp  47040  scmfsupp  47044  mptcfsupp  47046  lincresunit2  47149  itcoval0mpt  47342  eufsn  47498