Theorem mptex 6047

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 6046	. 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 1758   _Vcvv 3068   |-> cmpt 4448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4501  ax-sep 4511  ax-nul 4519  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524

This theorem is referenced by:  mptrabex  6048  eufnfv  6050  fvresex  6650  abrexex  6651  ofmres  6673  noinfep  7966  cantnffval  7970  cnfcomlem  8033  cnfcom3clem  8039  cnfcomlemOLD  8041  cnfcom3clemOLD  8047  fseqenlem1  8295  dfacacn  8411  dfac12lem1  8413  infmap2  8488  ackbij2lem2  8510  ackbij2lem3  8511  fin23lem32  8614  konigthlem  8833  wunex2  9006  wuncval2  9015  rpnnen1lem1  11080  rpnnen1lem3  11082  rpnnen1lem5  11084  ccatfval  12375  swrdval  12415  swrd00  12416  swrd0  12429  revval  12502  repsundef  12511  climmpt  13151  climle  13219  iserabs  13380  isumshft  13404  supcvg  13420  trireciplem  13426  expcnv  13428  explecnv  13429  geolim  13432  geo2lim  13437  cvgrat  13445  mertenslem2  13447  eftlub  13495  rpnnen2lem1  13599  rpnnen2lem2  13600  odzval  13965  1arithlem1  14086  1arith  14090  vdwapval  14136  vdwlem6  14149  vdwlem9  14152  restfn  14465  cidfval  14716  cidffn  14718  idfu2nd  14889  idfu1st  14891  idfucl  14893  fucco  14974  homafval  14999  idafval  15027  prf1  15112  prf2fval  15113  prfcl  15115  prf1st  15116  prf2nd  15117  curf1fval  15136  curf11  15138  curf12  15139  curf1cl  15140  curf2  15141  curfcl  15144  hof2val  15168  yonedalem3a  15186  yonedalem4a  15187  yonedalem4b  15188  yonedalem4c  15189  yonedalem3  15192  yonedainv  15193  lubfval  15250  glbfval  15263  grpinvfval  15678  grplactfval  15724  cntzfval  15940  pmtrfval  16058  psgnfval  16108  odfval  16140  sylow1lem2  16202  sylow2blem1  16223  sylow2blem2  16224  sylow3lem1  16230  sylow3lem6  16235  pj1fval  16295  vrgpfval  16367  dmdprd  16585  dprdval  16590  dprdvalOLD  16592  lspfval  17160  sraval  17363  aspval  17505  asclfval  17511  psrmulfval  17562  psrass1  17584  mvrval  17601  mplmon  17649  mplcoe1  17651  evlslem2  17704  mpfrcl  17711  evlsval  17712  evlsvar  17716  mpfind  17729  coe1fval  17768  psropprmul  17800  coe1mul2  17830  ply1coe  17855  ply1coeOLD  17856  evls1val  17864  evl1fval  17871  evl1val  17872  zrhval2  18049  submafval  18501  mdetfval  18508  madufval  18559  minmar1fval  18568  1stcfb  19165  ptbasfi  19270  dfac14  19307  fmval  19632  fmf  19634  flffval  19678  fcfval  19722  cnextval  19749  met1stc  20212  pcoval  20699  iscmet3lem3  20917  mbflimsup  21260  mbflim  21262  itg1climres  21308  mbfi1fseqlem2  21310  mbfi1fseqlem4  21312  mbfi1fseqlem6  21314  mbfi1flimlem  21316  mbfmullem2  21318  itg2monolem1  21344  itg2addlem  21352  itg2cnlem1  21355  cpnfval  21522  mdegfval  21647  ig1pval  21760  elply  21779  plyeq0lem  21794  plypf1  21796  geolim3  21921  ulmuni  21973  ulmcau  21976  ulmdvlem1  21981  ulmdvlem3  21983  mbfulm  21987  itgulm  21989  pserval  21991  dvradcnv  22002  pserdvlem2  22009  abelthlem1  22012  abelthlem3  22014  abelthlem6  22017  logtayl  22221  leibpi  22453  dfef2  22480  emcllem4  22508  emcllem6  22510  emcllem7  22511  basellem6  22539  sqff1o  22636  dchrptlem2  22720  dchrptlem3  22721  dchrisumlem3  22856  padicfval  22981  padicabvf  22996  istrkg2ld  23038  mirval  23185  axlowdim  23342  eupatrl  23724  nmoofval  24297  htthlem  24454  pjhfval  24934  pjmfn  25253  hosmval  25274  hommval  25275  hodmval  25276  hfsmval  25277  hfmmval  25278  eigvalfval  25436  brafval  25482  kbfval  25491  rnbra  25646  bra11  25647  fpwrelmap  26167  sgnsv  26324  ordtconlem1  26488  xrhval  26578  sxbrsigalem2  26835  sitgval  26852  eulerpart  26899  dstfrvclim1  26994  ballotlemfval  27006  ballotlemsval  27025  signstfv  27098  lgamgulmlem5  27153  lgamgulmlem6  27154  lgamcvg2  27175  cvmliftlem5  27312  circum  27453  divcnvshft  27532  divcnvlin  27533  climlec3  27535  faclimlem2  27684  faclim2  27688  ptrest  28563  voliunnfl  28573  volsupnfl  28574  upixp  28761  sdclem2  28776  fdc  28779  lmclim2  28792  geomcau  28793  rrncmslem  28869  mzpincl  29208  dfac11  29553  dfac21  29557  hbtlem1  29617  hbtlem7  29619  rgspnval  29663  addrval  29860  subrval  29861  mulvval  29862  fmuldfeqlem1  29901  fmuldfeq  29902  clim1fr1  29912  climexp  29916  climneg  29921  climdivf  29923  stoweidlem59  29992  wallispilem5  30002  wallispi  30003  stirlinglem1  30007  stirlinglem8  30014  stirlinglem14  30020  stirlinglem15  30021  wwlkn  30454  wlknwwlknbij2  30484  wlkiswwlkbij2  30491  wlknwwlknvbij  30510  clwwlkn  30568  clwwlknprop  30573  clwwlkbij  30599  clwwlkvbij  30601  numclwlk1lem2  30828  mptnn0fsupp  30940  pmatcollpw1lem4  31230  pmatcollpwlem  31233  lkrfval  33038  pmapfval  33706  pclfvalN  33839  polfvalN  33854  watfvalN  33942  ldilfset  34058  ltrnfset  34067  dilfsetN  34102  trnfsetN  34105  trlfset  34110  trlset  34111  tgrpfset  34694  tendofset  34708  tendopl  34726  tendoi  34744  erngfset  34749  erngfset-rN  34757  dvafset  34954  diaffval  34981  diafval  34982  dvhfset  35031  docaffvalN  35072  docafvalN  35073  djaffvalN  35084  dibffval  35091  dibfval  35092  dibopelvalN  35094  dibopelval2  35096  dibelval3  35098  dibn0  35104  dib0  35115  diblsmopel  35122  dicffval  35125  dicfval  35126  dicn0  35143  dihffval  35181  dihfval  35182  dihopelvalcpre  35199  dihatlat  35285  dihpN  35287  dochffval  35300  dochfval  35301  djhffval  35347  lcfrlem8  35500  lcfrlem9  35501  lcdfval  35539  mapdffval  35577  mapdfval  35578  hvmapffval  35709  hvmapfval  35710  hvmapval  35711  hdmap1ffval  35747  hdmap1fval  35748  hdmapffval  35780  hdmapfval  35781  hgmapffval  35839  hgmapfval  35840  hlhilset  35888