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

Theorem mptex 5958
Description: If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.)
Hypothesis
Ref Expression
mptex.1  |-  A  e. 
_V
Assertion
Ref Expression
mptex  |-  ( x  e.  A  |->  B )  e.  _V
Distinct variable group:    x, A
Allowed substitution hint:    B( x)

Proof of Theorem mptex
StepHypRef Expression
1 mptex.1 . 2  |-  A  e. 
_V
2 mptexg 5957 . 2  |-  ( A  e.  _V  ->  (
x  e.  A  |->  B )  e.  _V )
31, 2ax-mp 8 1  |-  ( x  e.  A  |->  B )  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2948    e. cmpt 4258
This theorem is referenced by:  eufnfv  5964  fvresex  5974  abrexex  5975  ofmres  6335  noinfep  7606  cantnffval  7610  cnfcomlem  7648  cnfcom3clem  7654  fseqenlem1  7897  dfacacn  8013  dfac12lem1  8015  infmap2  8090  ackbij2lem2  8112  ackbij2lem3  8113  fin23lem32  8216  konigthlem  8435  wunex2  8605  wuncval2  8614  rpnnen1lem1  10592  rpnnen1lem3  10594  rpnnen1lem5  10596  ccatfval  11734  swrdval  11756  swrd00  11757  revval  11784  climmpt  12357  climle  12425  iserabs  12586  isumshft  12611  supcvg  12627  trireciplem  12633  expcnv  12635  explecnv  12636  geolim  12639  geo2lim  12644  cvgrat  12652  mertenslem2  12654  eftlub  12702  rpnnen2lem1  12806  rpnnen2lem2  12807  odzval  13169  1arithlem1  13283  1arith  13287  vdwapval  13333  vdwlem6  13346  vdwlem9  13349  restfn  13644  cidfval  13893  cidffn  13895  idfu2nd  14066  idfu1st  14068  idfucl  14070  fucco  14151  homafval  14176  idafval  14204  prf1  14289  prf2fval  14290  prfcl  14292  prf1st  14293  prf2nd  14294  curf1fval  14313  curf11  14315  curf12  14316  curf1cl  14317  curf2  14318  curfcl  14321  hof2val  14345  yonedalem3a  14363  yonedalem4a  14364  yonedalem4b  14365  yonedalem4c  14366  yonedalem3  14369  yonedainv  14370  lubfval  14427  glbfval  14432  grpinvfval  14835  grplactfval  14877  cntzfval  15111  odfval  15163  sylow1lem2  15225  sylow2blem1  15246  sylow2blem2  15247  sylow3lem1  15253  sylow3lem6  15258  pj1fval  15318  vrgpfval  15390  dmdprd  15551  dprdval  15553  lspfval  16041  sraval  16240  aspval  16379  asclfval  16385  psrmulfval  16441  mvrval  16477  evlslem2  16560  coe1fval  16595  psropprmul  16624  ply1coe  16676  zrhval2  16782  1stcfb  17500  ptbasfi  17605  dfac14  17642  fmval  17967  fmf  17969  flffval  18013  fcfval  18057  cnextval  18084  met1stc  18543  pcoval  19028  iscmet3lem3  19235  mbflimsup  19550  mbflim  19552  itg1climres  19598  mbfi1fseqlem2  19600  mbfi1fseqlem4  19602  mbfi1fseqlem6  19604  mbfi1flimlem  19606  mbfmullem2  19608  itg2monolem1  19634  itg2addlem  19642  itg2cnlem1  19645  cpnfval  19810  mpfrcl  19931  evlsval  19932  evlsvar  19936  evl1fval  19939  evl1val  19940  mpfind  19957  mdegfval  19977  ig1pval  20087  elply  20106  plyeq0lem  20121  plypf1  20123  geolim3  20248  ulmuni  20300  ulmcau  20303  ulmdvlem1  20308  ulmdvlem3  20310  mbfulm  20314  itgulm  20316  pserval  20318  dvradcnv  20329  pserdvlem2  20336  abelthlem1  20339  abelthlem3  20341  abelthlem6  20344  logtayl  20543  leibpi  20774  dfef2  20801  emcllem4  20829  emcllem6  20831  emcllem7  20832  basellem6  20860  sqff1o  20957  dchrptlem2  21041  dchrptlem3  21042  dchrisumlem3  21177  padicfval  21302  padicabvf  21317  eupatrl  21682  nmoofval  22255  htthlem  22412  pjhfval  22890  pjmfn  23209  hosmval  23230  hommval  23231  hodmval  23232  hfsmval  23233  hfmmval  23234  eigvalfval  23392  brafval  23438  kbfval  23447  rnbra  23602  bra11  23603  xrhval  24376  sxbrsigalem2  24628  sitgval  24639  dstfrvclim1  24727  ballotlemfval  24739  ballotlemsval  24758  lgamgulmlem5  24809  lgamgulmlem6  24810  lgamcvg2  24831  cvmliftlem5  24968  circum  25103  divcnvshft  25203  divcnvlin  25204  climlec3  25206  faclimlem2  25355  faclim2  25359  axlowdim  25892  voliunnfl  26240  volsupnfl  26241  upixp  26422  sdclem2  26437  fdc  26440  lmclim2  26455  geomcau  26456  rrncmslem  26532  mzpincl  26782  dfac11  27128  dfac21  27132  hbtlem1  27295  hbtlem7  27297  rgspnval  27341  pmtrfval  27361  psgnfval  27391  mdetfval  27455  addrval  27638  subrval  27639  mulvval  27640  fmuldfeqlem1  27679  fmuldfeq  27680  clim1fr1  27694  climexp  27698  climneg  27703  climdivf  27705  stoweidlem59  27775  wallispilem5  27785  wallispi  27786  stirlinglem1  27790  stirlinglem8  27797  stirlinglem14  27803  stirlinglem15  27804  lkrfval  29822  pmapfval  30490  pclfvalN  30623  polfvalN  30638  watfvalN  30726  ldilfset  30842  ltrnfset  30851  dilfsetN  30886  trnfsetN  30889  trlfset  30894  trlset  30895  tgrpfset  31478  tendofset  31492  tendopl  31510  tendoi  31528  erngfset  31533  erngfset-rN  31541  dvafset  31738  diaffval  31765  diafval  31766  dvhfset  31815  docaffvalN  31856  docafvalN  31857  djaffvalN  31868  dibffval  31875  dibfval  31876  dibopelvalN  31878  dibopelval2  31880  dibelval3  31882  dibn0  31888  dib0  31899  diblsmopel  31906  dicffval  31909  dicfval  31910  dicn0  31927  dihffval  31965  dihfval  31966  dihopelvalcpre  31983  dihatlat  32069  dihpN  32071  dochffval  32084  dochfval  32085  djhffval  32131  lcfrlem8  32284  lcfrlem9  32285  lcdfval  32323  mapdffval  32361  mapdfval  32362  hvmapffval  32493  hvmapfval  32494  hvmapval  32495  hdmap1ffval  32531  hdmap1fval  32532  hdmapffval  32564  hdmapfval  32565  hgmapffval  32623  hgmapfval  32624  hlhilset  32672
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454
  Copyright terms: Public domain W3C validator