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

Theorem mptexg 5865
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 5393 . 2  |-  Fun  (
x  e.  A  |->  B )
2 eqid 2366 . . . 4  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
32dmmptss 5272 . . 3  |-  dom  (
x  e.  A  |->  B )  C_  A
4 ssexg 4262 . . 3  |-  ( ( dom  ( x  e.  A  |->  B )  C_  A  /\  A  e.  V
)  ->  dom  ( x  e.  A  |->  B )  e.  _V )
53, 4mpan 651 . 2  |-  ( A  e.  V  ->  dom  ( x  e.  A  |->  B )  e.  _V )
6 funex 5863 . 2  |-  ( ( Fun  ( x  e.  A  |->  B )  /\  dom  ( x  e.  A  |->  B )  e.  _V )  ->  ( x  e.  A  |->  B )  e. 
_V )
71, 5, 6sylancr 644 1  |-  ( A  e.  V  ->  (
x  e.  A  |->  B )  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1715   _Vcvv 2873    C_ wss 3238    e. cmpt 4179   dom cdm 4792   Fun wfun 5352
This theorem is referenced by:  mptex  5866  abrexexg  5884  xpexgALT  6197  offval  6212  offval3  6218  iunon  6497  onoviun  6502  mptelixpg  6996  infxpenc2lem2  7794  coftr  8046  axcc3  8211  seqof2  11268  ramcl  13284  restval  13541  prdsplusgval  13582  prdsmulrval  13584  prdsvscaval  13588  resf1st  13978  resf2nd  13979  funcres  13980  galactghm  14993  sylow1lem4  15122  sylow3lem2  15149  sylow3lem3  15150  dpjfval  15500  mvrfval  16375  opsrval  16426  ntrfval  16978  clsfval  16979  neifval  17053  lpfval  17087  ptcnplem  17532  upxp  17534  xkocnv  17722  fmfnfmlem3  17864  fmfnfmlem4  17865  ptcmplem3  17961  prdsdsf  18144  ressprdsds  18148  prdsxmslem2  18288  itgulm2  20003  pserulm  20016  grpoinvfval  21202  cnextval  23697  ustuqtoplem  23742  ustuqtop0  23743  utopsnneiplem  23750  indv  23875  indval  23876  ofcfval  23946  ofcfval3  23950  dstfrvclim1  24183  ptpcon  24367  vdgrfval  24476  tailfval  25828  upixp  25910  pw2f1ocnv  26636  kelac1  26667  frlmgsum  26738  uvcfval  26739  uvcval  26740  pmtrval  26900  pmtrrn  26905  pmtrfrn  26906  fmulcl  27217  fmuldfeqlem1  27218  stoweidlem31  27286  stoweidlem42  27297  stoweidlem48  27303  stoweidlem59  27314  nbgraf1o0  27612  cusgrafilem3  27646  vdgrefval  27805  frgrancvvdeqlem9  27876  bnj1366  28626
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-rep 4233  ax-sep 4243  ax-nul 4251  ax-pr 4316
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-reu 2635  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-iun 4009  df-br 4126  df-opab 4180  df-mpt 4181  df-id 4412  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366
  Copyright terms: Public domain W3C validator