Theorem mptexg 7164

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3438   ⊆ wss 3899   ↦ cmpt 5176  dom cdm 5621  Fun wfun 6483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497

This theorem is referenced by:  mptex  7166  mptexd  7167  ovmpt3rab1  7613  offval  7628  xpexgALT  7922  offval3  7923  suppssov1  8136  suppssov2  8137  suppssfv  8141  iunon  8268  onoviun  8272  mptelixpg  8868  cantnfp1lem1  9578  updjud  9837  coftr  10174  axcc3  10339  reps  14687  wrd2f1tovbij  14877  restval  17340  resf1st  17811  resf2nd  17812  funcres  17813  vrmdfval  18774  symgfixfolem1  19360  pmtrval  19373  pmtrrn  19379  pmtrfrn  19380  sylow1lem4  19523  sylow3lem2  19550  sylow3lem3  19551  funcrngcsetc  20565  funcringcsetc  20599  uvcfval  21731  uvcval  21732  uvcff  21738  uvcresum  21740  psrass1lem  21879  opsrval  21991  selvfval  22059  psropprmul  22160  mavmuldm  22475  mat2pmatfval  22648  cpm2mfval  22674  chpmatfval  22755  ntrfval  22949  clsfval  22950  neifval  23024  lpfval  23063  ptcnplem  23546  upxp  23548  fmfnfmlem3  23881  fmfnfmlem4  23882  ustuqtoplem  24164  ustuqtop0  24165  utopsnneiplem  24172  rrxmval  25342  tayl0  26306  itgulm2  26355  efabl  26496  tgjustr  28462  lmif  28773  islmib  28775  nbusgrf1o1  29359  cusgrfilem3  29447  vtxdgfval  29457  wlkiswwlks2  29864  wwlksnextbij  29891  clwlkclwwlklem1  29990  grpoinvfval  30513  acunirnmpt  32652  acunirnmpt2  32653  acunirnmpt2f  32654  aciunf1lem  32655  fnpreimac  32664  mptiffisupp  32685  indv  32844  indval  32845  frlmdim  33635  ofcfval3  34126  omsval  34317  carsgclctunlem2  34343  pmeasadd  34349  sitgclg  34366  bnj1366  34852  ptpconn  35288  fwddifval  36217  tailfval  36427  curfv  37650  matunitlindflem1  37666  matunitlindflem2  37667  upixp  37779  pw2f1ocnv  43144  kelac1  43170  rfovd  44108  fsovrfovd  44116  dssmapfvd  44124  dssmapfv2d  44125  fmulcl  45695  fmuldfeqlem1  45696  dvnmul  46055  dvnprodlem2  46059  stoweidlem31  46143  stoweidlem42  46154  stoweidlem48  46160  etransclem1  46347  etransclem4  46350  etransclem13  46359  etransclem17  46363  0ome  46641  hoicvr  46660  hsphoif  46688  hsphoival  46691  hoidmvlelem2  46708  hoidmvlelem3  46709  ovnhoilem1  46713  ovnhoilem2  46714  ovnlecvr2  46722  ovncvr2  46723  hoidifhspval2  46727  hspmbllem2  46739  fundcmpsurinjALT  47526  sprbisymrel  47613  uspgrbisymrelALT  48269  scmsuppss  48485  rmfsupp  48487  scmfsupp  48489  mptcfsupp  48491  lincresunit2  48593  itcoval0mpt  48781  eufsn  48956