Theorem mptexg 7209

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 6563	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2765	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6232	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5284	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 702	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 7207	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 598	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2145  Vcvv 3457   ⊆ wss 3907   ↦ cmpt 5186  dom cdm 5652  Fun wfun 6519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533

This theorem is referenced by:  mptex  7211  mptexd  7212  ovmpt3rab1  7658  offval  7673  xpexgALT  7966  offval3  7967  suppssov1  8181  suppssov2  8182  suppssfv  8186  iunon  8314  onoviun  8318  mptelixpg  8921  cantnfp1lem1  9635  updjud  9908  coftr  10245  axcc3  10410  indv  12211  indval  12212  reps  14797  wrd2f1tovbij  14987  restval  17469  resf1st  17941  resf2nd  17942  funcres  17943  vrmdfval  18905  symgfixfolem1  19499  pmtrval  19512  pmtrrn  19518  pmtrfrn  19519  sylow1lem4  19662  sylow3lem2  19689  sylow3lem3  19690  funcrngcsetc  20716  funcringcsetc  20750  uvcfval  21894  uvcval  21895  uvcff  21901  uvcresum  21903  psrass1lem  22043  opsrval  22157  selvfval  22230  psropprmul  22357  mavmuldm  22668  mat2pmatfval  22841  cpm2mfval  22867  chpmatfval  22948  ntrfval  23142  clsfval  23143  neifval  23217  lpfval  23256  ptcnplem  23739  upxp  23741  fmfnfmlem3  24074  fmfnfmlem4  24075  ustuqtoplem  24357  ustuqtop0  24358  utopsnneiplem  24365  rrxmval  25525  tayl0  26483  itgulm2  26530  efabl  26673  tgjustr  28701  lmif  29037  islmib  29039  nbusgrf1o1  29629  cusgrfilem3  29716  vtxdgfval  29726  wlkiswwlks2  30133  wwlksnextbij  30160  clwlkclwwlklem1  30259  grpoinvfval  30783  acunirnmpt  32916  acunirnmpt2  32917  acunirnmpt2f  32918  aciunf1lem  32919  fnpreimac  32927  mptiffisupp  32950  frlmdim  33918  ofcfval3  34409  omsval  34600  carsgclctunlem2  34626  pmeasadd  34632  sitgclg  34649  bnj1366  35134  ptpconn  35596  fwddifval  36525  tailfval  36745  curfv  38111  matunitlindflem1  38127  matunitlindflem2  38128  upixp  38240  pw2f1ocnv  43626  kelac1  43652  rfovd  44589  fsovrfovd  44597  dssmapfvd  44605  dssmapfv2d  44606  fmulcl  46155  fmuldfeqlem1  46156  dvnmul  46515  dvnprodlem2  46519  stoweidlem31  46603  stoweidlem42  46614  stoweidlem48  46620  etransclem1  46807  etransclem4  46810  etransclem13  46819  etransclem17  46823  0ome  47101  hsphoif  47148  hsphoival  47151  hoidmvlelem2  47168  hoidmvlelem3  47169  ovnhoilem1  47173  ovnhoilem2  47174  ovnlecvr2  47182  ovncvr2  47183  hoidifhspval2  47187  hspmbllem2  47199  fundcmpsurinjALT  48016  sprbisymrel  48103  uspgrbisymrelALT  48775  scmsuppss  49002  rmfsupp  49004  scmfsupp  49006  mptcfsupp  49008  lincresunit2  49109  itcoval0mpt  49297  eufsn  49471