MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mptexg Structured version   Unicode version

Theorem mptexg 5959
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  |-  ( A  e.  V  ->  (
x  e.  A  |->  B )  e.  _V )
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    V( x)

Proof of Theorem mptexg
StepHypRef Expression
1 funmpt 5466 . 2  |-  Fun  (
x  e.  A  |->  B )
2 eqid 2443 . . . 4  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
32dmmptss 5346 . . 3  |-  dom  (
x  e.  A  |->  B )  C_  A
4 ssexg 4450 . . 3  |-  ( ( dom  ( x  e.  A  |->  B )  C_  A  /\  A  e.  V
)  ->  dom  ( x  e.  A  |->  B )  e.  _V )
53, 4mpan 670 . 2  |-  ( A  e.  V  ->  dom  ( x  e.  A  |->  B )  e.  _V )
6 funex 5957 . 2  |-  ( ( Fun  ( x  e.  A  |->  B )  /\  dom  ( x  e.  A  |->  B )  e.  _V )  ->  ( x  e.  A  |->  B )  e. 
_V )
71, 5, 6sylancr 663 1  |-  ( A  e.  V  ->  (
x  e.  A  |->  B )  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   _Vcvv 2984    C_ wss 3340    e. cmpt 4362   dom cdm 4852   Fun wfun 5424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4415  ax-sep 4425  ax-nul 4433  ax-pr 4543
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-reu 2734  df-rab 2736  df-v 2986  df-sbc 3199  df-csb 3301  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-iun 4185  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-fo 5436  df-f1o 5437  df-fv 5438
This theorem is referenced by:  mptex  5960  offval  6339  abrexexg  6564  xpexgALT  6582  offval3  6583  mptsuppdifd  6723  suppssov1  6733  suppssfv  6737  mpt2curryvald  6801  iunon  6811  onoviun  6816  mptelixpg  7312  fsuppmptif  7661  sniffsupp  7671  cantnfrescl  7896  cantnfp1lem1  7898  cantnflem1d  7908  cantnflem1  7909  infxpenc2lem2  8198  infxpenc2lem2OLD  8202  coftr  8454  axcc3  8619  seqof2  11876  reps  12420  ramcl  14102  restval  14377  prdsplusgval  14423  prdsmulrval  14425  prdsvscaval  14429  resf1st  14816  resf2nd  14817  funcres  14818  galactghm  15920  symgfixfolem1  15956  pmtrval  15969  pmtrrn  15975  pmtrfrn  15976  sylow1lem4  16112  sylow3lem2  16139  sylow3lem3  16140  gsummptfsaddOLD  16427  gsum2dlem2  16474  gsum2d  16475  dprdfinv  16521  dprdfadd  16522  dmdprdsplitlem  16546  dpjfval  16566  dpjidcl  16569  mptscmfsupp0  17023  psrass1lem  17459  psrridm  17488  psrdi  17491  psrdir  17492  psrcom  17493  mvrfval  17505  mplcoe5  17560  mplbas2  17563  opsrval  17568  evlslem6  17610  psropprmul  17705  evls1fval  17766  evls1sca  17770  frlmgsumOLD  18207  frlmgsum  18208  frlmphllem  18217  uvcfval  18221  uvcval  18222  uvcff  18228  uvcresum  18230  mvmulval  18366  mavmuldm  18373  mavmul0g  18376  marepvval0  18389  ntrfval  18640  clsfval  18641  neifval  18715  lpfval  18754  ptcnplem  19206  upxp  19208  xkocnv  19399  fmfnfmlem3  19541  fmfnfmlem4  19542  ptcmplem3  19638  ustuqtoplem  19826  ustuqtop0  19827  utopsnneiplem  19834  prdsdsf  19954  ressprdsds  19958  prdsxmslem2  20116  rrxmval  20916  tdeglem4  21541  tayl0  21839  itgulm2  21886  pserulm  21899  nbgraf1o0  23367  cusgrafilem3  23401  vdgrfval  23577  grpoinvfval  23723  indv  26481  indval  26482  ofcfval  26552  ofcfval3  26556  omsval  26720  ptpcon  27134  tailfval  28605  upixp  28635  pw2f1ocnv  29398  kelac1  29428  fmulcl  29774  fmuldfeqlem1  29775  stoweidlem31  29838  stoweidlem42  29849  stoweidlem48  29855  ovmpt3rab1  30173  wrd2f1tovbij  30267  wlkiswwlk2  30343  wwlkextbij  30377  clwlkisclwwlklem2  30460  clwlksizeeq  30537  frgrancvvdeqlem9  30646  numclwwlk2lem3  30711  scmsuppss  30797  rmfsupp  30800  scmfsupp  30804  mptcfsupp  30806  matgsum  30874  lincresunit2  31024  bnj1366  31835
  Copyright terms: Public domain W3C validator