Theorem mptex 6152

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 6151	. 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 1904   _Vcvv 3031   |-> cmpt 4454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597

This theorem is referenced by:  mptrabex  6153  mptrabexOLD  6154  eufnfv  6156  fvresex  6785  abrexex  6786  ofmres  6808  noinfep  8183  cantnffval  8186  cnfcomlem  8222  cnfcom3clem  8228  fseqenlem1  8473  dfacacn  8589  dfac12lem1  8591  infmap2  8666  ackbij2lem2  8688  ackbij2lem3  8689  fin23lem32  8792  konigthlem  9011  wunex2  9181  wuncval2  9190  rpnnen1lem1  11313  rpnnen1lem3  11315  rpnnen1lem5  11317  mptnn0fsupp  12247  ccatfn  12768  ccatfval  12770  swrdval  12827  swrd00  12828  swrd0  12844  revval  12919  repsundef  12928  climmpt  13712  climle  13780  iserabs  13952  isumshft  13974  divcnvshft  13990  supcvg  13991  trireciplem  13997  expcnv  13999  explecnv  14000  geolim  14003  geo2lim  14008  cvgrat  14016  mertenslem2  14018  eftlub  14240  rpnnen2lem1  14344  rpnnen2lem2  14345  1arithlem1  14946  1arith  14950  vdwapval  15002  vdwlem6  15015  vdwlem9  15018  restfn  15401  cidfval  15660  cidffn  15662  idfu2nd  15860  idfu1st  15862  idfucl  15864  fucco  15945  homafval  16002  idafval  16030  prf1  16163  prf2fval  16164  prfcl  16166  prf1st  16167  prf2nd  16168  curf1fval  16187  curf11  16189  curf12  16190  curf1cl  16191  curf2  16192  curfcl  16195  hof2val  16219  yonedalem3a  16237  yonedalem4a  16238  yonedalem4b  16239  yonedalem4c  16240  yonedalem3  16243  yonedainv  16244  lubfval  16302  glbfval  16315  grpinvfval  16782  grplactfval  16830  cntzfval  17052  psgnfval  17219  odfval  17257  odfvalOLD  17260  sylow1lem2  17329  sylow2blem1  17350  sylow2blem2  17351  sylow3lem1  17357  sylow3lem6  17362  pj1fval  17422  vrgpfval  17494  lspfval  18274  sraval  18477  aspval  18629  asclfval  18635  psrmulfval  18686  psrass1  18706  mvrval  18722  mplmon  18764  mplcoe1  18766  evlslem2  18812  mpfrcl  18818  evlsval  18819  evlsvar  18823  mpfind  18836  coe1fval  18875  psropprmul  18908  coe1mul2  18939  ply1coe  18966  ply1coeOLD  18967  evls1fval  18985  evls1val  18986  evl1fval  18993  evl1val  18994  zrhval2  19157  submafval  19681  mdetfval  19688  madufval  19739  minmar1fval  19748  pmatcollpw2lem  19878  pm2mpval  19896  1stcfb  20537  ptbasfi  20673  dfac14  20710  fmval  21036  fmf  21038  flffval  21082  fcfval  21126  cnextval  21154  met1stc  21614  pcoval  22120  iscmet3lem3  22338  mbflimsup  22702  mbflimsupOLD  22703  mbflim  22705  itg1climres  22751  mbfi1fseqlem2  22753  mbfi1fseqlem4  22755  mbfi1fseqlem6  22757  mbfi1flimlem  22759  mbfmullem2  22761  itg2monolem1  22787  itg2addlem  22795  itg2cnlem1  22798  cpnfval  22965  mdegfval  23090  ig1pval  23203  ig1pvalOLD  23209  elply  23228  plyeq0lem  23243  plypf1  23245  geolim3  23374  ulmuni  23426  ulmcau  23429  ulmdvlem1  23434  ulmdvlem3  23436  mbfulm  23440  itgulm  23442  pserval  23444  dvradcnv  23455  pserdvlem2  23462  abelthlem1  23465  abelthlem3  23467  abelthlem6  23470  logtayl  23684  leibpi  23947  dfef2  23975  emcllem4  24003  emcllem6  24005  emcllem7  24006  lgamgulmlem5  24037  lgamgulmlem6  24038  lgamcvg2  24059  basellem6  24091  sqff1o  24188  dchrptlem2  24272  dchrptlem3  24273  dchrisumlem3  24408  padicfval  24533  padicabvf  24548  istrkg2ld  24587  ishlg  24726  mirval  24779  ishpg  24880  lmif  24906  islmib  24908  axlowdim  25070  wwlkn  25489  clwwlkn  25574  clwwlknprop  25579  eupatrl  25775  numclwlk1lem2  25904  nmoofval  26484  htthlem  26651  pjhfval  27130  pjmfn  27449  hosmval  27469  hommval  27470  hodmval  27471  hfsmval  27472  hfmmval  27473  eigvalfval  27631  brafval  27677  kbfval  27686  rnbra  27841  bra11  27842  padct  28382  fpwrelmap  28393  sgnsv  28564  locfinreflem  28741  ordtconlem1  28804  xrhval  28896  sigapildsys  29058  sxbrsigalem2  29181  eulerpart  29288  dstfrvclim1  29383  ballotlemfval  29395  ballotlemsval  29414  ballotlemsvalOLD  29452  signstfv  29524  cvmliftlem5  30084  mvrsval  30215  mrsubffval  30217  mrsubfval  30218  msubffval  30233  msubfval  30234  msubrn  30239  msubco  30241  mvhfval  30243  msrfval  30247  msubvrs  30270  circum  30390  divcnvlin  30438  climlec3  30440  faclimlem2  30451  faclim2  30455  ptrest  32003  poimirlem17  32021  poimirlem20  32024  voliunnfl  32048  volsupnfl  32049  upixp  32120  sdclem2  32135  fdc  32138  lmclim2  32151  geomcau  32152  rrncmslem  32228  lkrfval  32724  pmapfval  33392  pclfvalN  33525  polfvalN  33540  watfvalN  33628  ldilfset  33744  ltrnfset  33753  dilfsetN  33789  trnfsetN  33792  trlfset  33797  trlset  33798  tgrpfset  34382  tendofset  34396  tendopl  34414  tendoi  34432  erngfset  34437  erngfset-rN  34445  dvafset  34642  diaffval  34669  dvhfset  34719  docaffvalN  34760  docafvalN  34761  djaffvalN  34772  dibffval  34779  dibfval  34780  dibopelvalN  34782  dibopelval2  34784  dibelval3  34786  dibn0  34792  dib0  34803  diblsmopel  34810  dicffval  34813  dicn0  34831  dihffval  34869  dihfval  34870  dihopelvalcpre  34887  dihatlat  34973  dihpN  34975  dochffval  34988  dochfval  34989  djhffval  35035  lcfrlem8  35188  lcfrlem9  35189  lcdfval  35227  mapdffval  35265  mapdfval  35266  hvmapffval  35397  hvmapfval  35398  hvmapval  35399  hdmap1ffval  35435  hdmap1fval  35436  hdmapffval  35468  hdmapfval  35469  hgmapffval  35527  hgmapfval  35528  hlhilset  35576  mzpincl  35647  dfac11  35991  dfac21  35995  hbtlem1  36053  hbtlem7  36055  rgspnval  36105  dvgrat  36731  radcnvrat  36733  hashnzfzclim  36741  uzmptshftfval  36765  dvradcnv2  36766  binomcxplemrat  36769  binomcxplemcvg  36773  binomcxplemdvsum  36774  binomcxplemnotnn0  36775  addrval  36889  subrval  36890  mulvval  36891  fmuldfeqlem1  37757  fmuldfeq  37758  clim1fr1  37776  climexp  37780  climneg  37786  climdivf  37789  divcnvg  37804  expfac  37835  dvsinax  37880  dvcosax  37895  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  dvnprodlem1  37918  dvnprodlem2  37919  dvnprodlem3  37920  stoweidlem59  38032  wallispilem5  38043  wallispi  38044  stirlinglem1  38048  stirlinglem8  38055  stirlinglem14  38061  stirlinglem15  38062  dirkerval  38065  fourierdlem71  38153  fourierdlem103  38185  fourierdlem104  38186  fourierdlem112  38194  etransclem48OLD  38259  etransclem48  38260  salgensscntex  38315  sge0tsms  38336  nnfoctbdjlem  38409  isomenndlem  38470  ovnval  38481  ovncvrrp  38504  ovnsubaddlem1  38510  hsphoif  38516  hsphoival  38519  ovnhoilem2  38542  hoidifhspval  38548  ovncvr2  38551  hspmbllem2  38567  vtxdushgrfvedglem  39712  vtxdushgrfvedg  39713  crctcshlem3  39997  irinitoringc  40579  aacllem  41046