Theorem mptex 6142

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

Step	Hyp	Ref	Expression
1		mptex.1	. 2 |- A e. _V
2		mptexg 6141	. 2 |- ( A e. _V -> ( x e. A |-> B ) e. _V )
3	1, 2	ax-mp 5	1 |- ( x e. A |-> B ) e. _V

Syntax hints:   e. wcel 1867   _Vcvv 3078   |-> cmpt 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4529  ax-sep 4539  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600

This theorem is referenced by:  mptrabex  6143  eufnfv  6145  fvresex  6771  abrexex  6772  ofmres  6794  noinfep  8155  cantnffval  8158  cnfcomlem  8194  cnfcom3clem  8200  fseqenlem1  8444  dfacacn  8560  dfac12lem1  8562  infmap2  8637  ackbij2lem2  8659  ackbij2lem3  8660  fin23lem32  8763  konigthlem  8982  wunex2  9152  wuncval2  9161  rpnnen1lem1  11279  rpnnen1lem3  11281  rpnnen1lem5  11283  mptnn0fsupp  12195  ccatfn  12693  ccatfval  12695  swrdval  12747  swrd00  12748  swrd0  12764  revval  12839  repsundef  12848  climmpt  13602  climle  13670  iserabs  13842  isumshft  13864  divcnvshft  13880  supcvg  13881  trireciplem  13887  expcnv  13889  explecnv  13890  geolim  13893  geo2lim  13898  cvgrat  13906  mertenslem2  13908  eftlub  14130  rpnnen2lem1  14234  rpnnen2lem2  14235  1arithlem1  14819  1arith  14823  vdwapval  14875  vdwlem6  14888  vdwlem9  14891  restfn  15275  cidfval  15526  cidffn  15528  idfu2nd  15726  idfu1st  15728  idfucl  15730  fucco  15811  homafval  15868  idafval  15896  prf1  16029  prf2fval  16030  prfcl  16032  prf1st  16033  prf2nd  16034  curf1fval  16053  curf11  16055  curf12  16056  curf1cl  16057  curf2  16058  curfcl  16061  hof2val  16085  yonedalem3a  16103  yonedalem4a  16104  yonedalem4b  16105  yonedalem4c  16106  yonedalem3  16109  yonedainv  16110  lubfval  16168  glbfval  16181  grpinvfval  16648  grplactfval  16696  cntzfval  16918  psgnfval  17085  odfval  17117  sylow1lem2  17179  sylow2blem1  17200  sylow2blem2  17201  sylow3lem1  17207  sylow3lem6  17212  pj1fval  17272  vrgpfval  17344  lspfval  18124  sraval  18327  aspval  18480  asclfval  18486  psrmulfval  18537  psrass1  18557  mvrval  18573  mplmon  18615  mplcoe1  18617  evlslem2  18663  mpfrcl  18669  evlsval  18670  evlsvar  18674  mpfind  18687  coe1fval  18726  psropprmul  18759  coe1mul2  18790  ply1coe  18817  ply1coeOLD  18818  evls1fval  18836  evls1val  18837  evl1fval  18844  evl1val  18845  zrhval2  19004  submafval  19528  mdetfval  19535  madufval  19586  minmar1fval  19595  pmatcollpw2lem  19725  pm2mpval  19743  1stcfb  20384  ptbasfi  20520  dfac14  20557  fmval  20882  fmf  20884  flffval  20928  fcfval  20972  cnextval  21000  met1stc  21460  pcoval  21928  iscmet3lem3  22146  mbflimsup  22497  mbflimsupOLD  22498  mbflim  22500  itg1climres  22546  mbfi1fseqlem2  22548  mbfi1fseqlem4  22550  mbfi1fseqlem6  22552  mbfi1flimlem  22554  mbfmullem2  22556  itg2monolem1  22582  itg2addlem  22590  itg2cnlem1  22593  cpnfval  22760  mdegfval  22885  ig1pval  22995  elply  23014  plyeq0lem  23029  plypf1  23031  geolim3  23157  ulmuni  23209  ulmcau  23212  ulmdvlem1  23217  ulmdvlem3  23219  mbfulm  23223  itgulm  23225  pserval  23227  dvradcnv  23238  pserdvlem2  23245  abelthlem1  23248  abelthlem3  23250  abelthlem6  23253  logtayl  23467  leibpi  23730  dfef2  23758  emcllem4  23786  emcllem6  23788  emcllem7  23789  lgamgulmlem5  23820  lgamgulmlem6  23821  lgamcvg2  23842  basellem6  23872  sqff1o  23969  dchrptlem2  24053  dchrptlem3  24054  dchrisumlem3  24189  padicfval  24314  padicabvf  24329  istrkg2ld  24368  ishlg  24504  mirval  24557  ishpg  24654  lmif  24680  islmib  24682  axlowdim  24834  wwlkn  25252  clwwlkn  25337  clwwlknprop  25342  eupatrl  25538  numclwlk1lem2  25667  nmoofval  26245  htthlem  26402  pjhfval  26881  pjmfn  27200  hosmval  27220  hommval  27221  hodmval  27222  hfsmval  27223  hfmmval  27224  eigvalfval  27382  brafval  27428  kbfval  27437  rnbra  27592  bra11  27593  padct  28147  fpwrelmap  28158  sgnsv  28325  locfinreflem  28503  ordtconlem1  28566  xrhval  28658  sigapildsys  28820  sxbrsigalem2  28944  eulerpart  29038  dstfrvclim1  29133  ballotlemfval  29145  ballotlemsval  29164  signstfv  29237  cvmliftlem5  29797  mvrsval  29928  mrsubffval  29930  mrsubfval  29931  msubffval  29946  msubfval  29947  msubrn  29952  msubco  29954  mvhfval  29956  msrfval  29960  msubvrs  29983  circum  30103  divcnvlin  30151  climlec3  30153  faclimlem2  30164  faclim2  30168  ptrest  31643  poimirlem17  31661  poimirlem20  31664  voliunnfl  31688  volsupnfl  31689  upixp  31760  sdclem2  31775  fdc  31778  lmclim2  31791  geomcau  31792  rrncmslem  31868  lkrfval  32362  pmapfval  33030  pclfvalN  33163  polfvalN  33178  watfvalN  33266  ldilfset  33382  ltrnfset  33391  dilfsetN  33427  trnfsetN  33430  trlfset  33435  trlset  33436  tgrpfset  34020  tendofset  34034  tendopl  34052  tendoi  34070  erngfset  34075  erngfset-rN  34083  dvafset  34280  diaffval  34307  dvhfset  34357  docaffvalN  34398  docafvalN  34399  djaffvalN  34410  dibffval  34417  dibfval  34418  dibopelvalN  34420  dibopelval2  34422  dibelval3  34424  dibn0  34430  dib0  34441  diblsmopel  34448  dicffval  34451  dicn0  34469  dihffval  34507  dihfval  34508  dihopelvalcpre  34525  dihatlat  34611  dihpN  34613  dochffval  34626  dochfval  34627  djhffval  34673  lcfrlem8  34826  lcfrlem9  34827  lcdfval  34865  mapdffval  34903  mapdfval  34904  hvmapffval  35035  hvmapfval  35036  hvmapval  35037  hdmap1ffval  35073  hdmap1fval  35074  hdmapffval  35106  hdmapfval  35107  hgmapffval  35165  hgmapfval  35166  hlhilset  35214  mzpincl  35285  dfac11  35630  dfac21  35634  hbtlem1  35692  hbtlem7  35694  rgspnval  35737  dvgrat  36302  radcnvrat  36304  hashnzfzclim  36312  uzmptshftfval  36336  dvradcnv2  36337  binomcxplemrat  36340  binomcxplemcvg  36344  binomcxplemdvsum  36345  binomcxplemnotnn0  36346  addrval  36460  subrval  36461  mulvval  36462  fmuldfeqlem1  37236  fmuldfeq  37237  clim1fr1  37255  climexp  37259  climneg  37265  climdivf  37268  divcnvg  37283  expfac  37314  dvsinax  37359  dvcosax  37374  ioodvbdlimc1lem2  37380  ioodvbdlimc2lem  37382  dvnprodlem1  37394  dvnprodlem2  37395  dvnprodlem3  37396  stoweidlem59  37493  wallispilem5  37504  wallispi  37505  stirlinglem1  37509  stirlinglem8  37516  stirlinglem14  37522  stirlinglem15  37523  dirkerval  37526  fourierdlem71  37613  fourierdlem103  37645  fourierdlem104  37646  fourierdlem112  37654  etransclem48  37718  sge0tsms  37760  nnfoctbdjlem  37806  irinitoringc  38842  aacllem  39314