Theorem mptex 5935

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 5934	. 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 1755   _Vcvv 2962   e. cmpt 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414

This theorem is referenced by:  mptrabex  5936  eufnfv  5938  fvresex  6539  abrexex  6540  ofmres  6562  noinfep  7853  cantnffval  7857  cnfcomlem  7920  cnfcom3clem  7926  cnfcomlemOLD  7928  cnfcom3clemOLD  7934  fseqenlem1  8182  dfacacn  8298  dfac12lem1  8300  infmap2  8375  ackbij2lem2  8397  ackbij2lem3  8398  fin23lem32  8501  konigthlem  8720  wunex2  8893  wuncval2  8902  rpnnen1lem1  10967  rpnnen1lem3  10969  rpnnen1lem5  10971  ccatfval  12257  swrdval  12297  swrd00  12298  swrd0  12311  revval  12384  repsundef  12393  climmpt  13033  climle  13101  iserabs  13261  isumshft  13285  supcvg  13301  trireciplem  13307  expcnv  13309  explecnv  13310  geolim  13313  geo2lim  13318  cvgrat  13326  mertenslem2  13328  eftlub  13376  rpnnen2lem1  13480  rpnnen2lem2  13481  odzval  13846  1arithlem1  13967  1arith  13971  vdwapval  14017  vdwlem6  14030  vdwlem9  14033  restfn  14346  cidfval  14597  cidffn  14599  idfu2nd  14770  idfu1st  14772  idfucl  14774  fucco  14855  homafval  14880  idafval  14908  prf1  14993  prf2fval  14994  prfcl  14996  prf1st  14997  prf2nd  14998  curf1fval  15017  curf11  15019  curf12  15020  curf1cl  15021  curf2  15022  curfcl  15025  hof2val  15049  yonedalem3a  15067  yonedalem4a  15068  yonedalem4b  15069  yonedalem4c  15070  yonedalem3  15073  yonedainv  15074  lubfval  15131  glbfval  15144  grpinvfval  15556  grplactfval  15602  cntzfval  15818  pmtrfval  15936  psgnfval  15986  odfval  16016  sylow1lem2  16078  sylow2blem1  16099  sylow2blem2  16100  sylow3lem1  16106  sylow3lem6  16111  pj1fval  16171  vrgpfval  16243  dmdprd  16454  dprdval  16459  dprdvalOLD  16461  lspfval  16976  sraval  17179  aspval  17321  asclfval  17327  psrmulfval  17390  psrass1  17412  mvrval  17428  mplmon  17476  mplcoe1  17478  evlslem2  17525  coe1fval  17560  psropprmul  17591  coe1mul2  17621  ply1coe  17643  zrhval2  17782  submafval  18232  mdetfval  18239  madufval  18285  minmar1fval  18294  1stcfb  18891  ptbasfi  18996  dfac14  19033  fmval  19358  fmf  19360  flffval  19404  fcfval  19448  cnextval  19475  met1stc  19938  pcoval  20425  iscmet3lem3  20643  mbflimsup  20986  mbflim  20988  itg1climres  21034  mbfi1fseqlem2  21036  mbfi1fseqlem4  21038  mbfi1fseqlem6  21040  mbfi1flimlem  21042  mbfmullem2  21044  itg2monolem1  21070  itg2addlem  21078  itg2cnlem1  21081  cpnfval  21248  mpfrcl  21370  evlsval  21371  evlsvar  21375  evl1fval  21378  evl1val  21379  mpfind  21396  mdegfval  21416  ig1pval  21529  elply  21548  plyeq0lem  21563  plypf1  21565  geolim3  21690  ulmuni  21742  ulmcau  21745  ulmdvlem1  21750  ulmdvlem3  21752  mbfulm  21756  itgulm  21758  pserval  21760  dvradcnv  21771  pserdvlem2  21778  abelthlem1  21781  abelthlem3  21783  abelthlem6  21786  logtayl  21990  leibpi  22222  dfef2  22249  emcllem4  22277  emcllem6  22279  emcllem7  22280  basellem6  22308  sqff1o  22405  dchrptlem2  22489  dchrptlem3  22490  dchrisumlem3  22625  padicfval  22750  padicabvf  22765  mirval  22925  axlowdim  23030  eupatrl  23412  nmoofval  23985  htthlem  24142  pjhfval  24622  pjmfn  24941  hosmval  24962  hommval  24963  hodmval  24964  hfsmval  24965  hfmmval  24966  eigvalfval  25124  brafval  25170  kbfval  25179  rnbra  25334  bra11  25335  fpwrelmap  25858  sgnsv  26014  ordtconlem1  26208  xrhval  26298  sxbrsigalem2  26555  sitgval  26566  eulerpart  26613  dstfrvclim1  26708  ballotlemfval  26720  ballotlemsval  26739  signstfv  26812  lgamgulmlem5  26867  lgamgulmlem6  26868  lgamcvg2  26889  cvmliftlem5  27026  circum  27166  divcnvshft  27245  divcnvlin  27246  climlec3  27248  faclimlem2  27397  faclim2  27401  ptrest  28269  voliunnfl  28279  volsupnfl  28280  upixp  28467  sdclem2  28482  fdc  28485  lmclim2  28498  geomcau  28499  rrncmslem  28575  mzpincl  28915  dfac11  29260  dfac21  29264  hbtlem1  29324  hbtlem7  29326  rgspnval  29370  addrval  29567  subrval  29568  mulvval  29569  fmuldfeqlem1  29608  fmuldfeq  29609  clim1fr1  29620  climexp  29624  climneg  29629  climdivf  29631  stoweidlem59  29700  wallispilem5  29710  wallispi  29711  stirlinglem1  29715  stirlinglem8  29722  stirlinglem14  29728  stirlinglem15  29729  wwlkn  30162  wlknwwlknbij2  30192  wlkiswwlkbij2  30199  wlknwwlknvbij  30218  clwwlkn  30276  clwwlknprop  30281  clwwlkbij  30307  clwwlkvbij  30309  numclwlk1lem2  30536  lkrfval  32326  pmapfval  32994  pclfvalN  33127  polfvalN  33142  watfvalN  33230  ldilfset  33346  ltrnfset  33355  dilfsetN  33390  trnfsetN  33393  trlfset  33398  trlset  33399  tgrpfset  33982  tendofset  33996  tendopl  34014  tendoi  34032  erngfset  34037  erngfset-rN  34045  dvafset  34242  diaffval  34269  diafval  34270  dvhfset  34319  docaffvalN  34360  docafvalN  34361  djaffvalN  34372  dibffval  34379  dibfval  34380  dibopelvalN  34382  dibopelval2  34384  dibelval3  34386  dibn0  34392  dib0  34403  diblsmopel  34410  dicffval  34413  dicfval  34414  dicn0  34431  dihffval  34469  dihfval  34470  dihopelvalcpre  34487  dihatlat  34573  dihpN  34575  dochffval  34588  dochfval  34589  djhffval  34635  lcfrlem8  34788  lcfrlem9  34789  lcdfval  34827  mapdffval  34865  mapdfval  34866  hvmapffval  34997  hvmapfval  34998  hvmapval  34999  hdmap1ffval  35035  hdmap1fval  35036  hdmapffval  35068  hdmapfval  35069  hgmapffval  35127  hgmapfval  35128  hlhilset  35176