Theorem mptex 6486

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 6484. (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 6484	. 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 1990   _Vcvv 3200   |-> cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896

This theorem is referenced by:  mptrabex  6488  mptrabexOLD  6489  eufnfv  6491  fvresex  7139  abrexexOLD  7142  ofmres  7164  noinfep  8557  cantnffval  8560  cnfcomlem  8596  cnfcom3clem  8602  fseqenlem1  8847  dfacacn  8963  dfac12lem1  8965  infmap2  9040  ackbij2lem2  9062  ackbij2lem3  9063  fin23lem32  9166  konigthlem  9390  wunex2  9560  wuncval2  9569  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  mptnn0fsupp  12797  ccatfn  13357  ccatfval  13358  swrdval  13417  swrd00  13418  swrd0  13434  revval  13509  repsundef  13518  climmpt  14302  climle  14370  iserabs  14547  isumshft  14571  divcnvshft  14587  supcvg  14588  trireciplem  14594  expcnv  14596  explecnv  14597  geolim  14601  geo2lim  14606  cvgrat  14615  mertenslem2  14617  eftlub  14839  rpnnen2lem1  14943  rpnnen2lem2  14944  1arithlem1  15627  1arith  15631  vdwapval  15677  vdwlem6  15690  vdwlem9  15693  restfn  16085  cidfval  16337  cidffn  16339  idfu2nd  16537  idfu1st  16539  idfucl  16541  fucco  16622  homafval  16679  idafval  16707  prf1  16840  prf2fval  16841  prfcl  16843  prf1st  16844  prf2nd  16845  curf1fval  16864  curf11  16866  curf12  16867  curf1cl  16868  curf2  16869  curfcl  16872  hof2val  16896  yonedalem3a  16914  yonedalem4a  16915  yonedalem4b  16916  yonedalem4c  16917  yonedalem3  16920  yonedainv  16921  lubfval  16978  glbfval  16991  grpinvfval  17460  grplactfval  17516  cntzfval  17753  psgnfval  17920  odfval  17952  sylow1lem2  18014  sylow2blem1  18035  sylow2blem2  18036  sylow3lem1  18042  sylow3lem6  18047  pj1fval  18107  vrgpfval  18179  lspfval  18973  sraval  19176  aspval  19328  asclfval  19334  psrmulfval  19385  psrass1  19405  mvrval  19421  mplmon  19463  mplcoe1  19465  evlslem2  19512  mpfrcl  19518  evlsval  19519  evlsvar  19523  mpfind  19536  coe1fval  19575  psropprmul  19608  coe1mul2  19639  ply1coe  19666  evls1fval  19684  evls1val  19685  evl1fval  19692  evl1val  19693  zrhval2  19857  submafval  20385  mdetfval  20392  madufval  20443  minmar1fval  20452  pmatcollpw2lem  20582  pm2mpval  20600  1stcfb  21248  ptbasfi  21384  dfac14  21421  fmval  21747  fmf  21749  flffval  21793  fcfval  21837  cnextval  21865  met1stc  22326  pcoval  22811  iscmet3lem3  23088  mbflimsup  23433  mbflim  23435  itg1climres  23481  mbfi1fseqlem2  23483  mbfi1fseqlem4  23485  mbfi1fseqlem6  23487  mbfi1flimlem  23489  mbfmullem2  23491  itg2monolem1  23517  itg2addlem  23525  itg2cnlem1  23528  cpnfval  23695  mdegfval  23822  ig1pval  23932  elply  23951  plyeq0lem  23966  plypf1  23968  geolim3  24094  ulmuni  24146  ulmcau  24149  ulmdvlem1  24154  ulmdvlem3  24156  mbfulm  24160  itgulm  24162  pserval  24164  dvradcnv  24175  pserdvlem2  24182  abelthlem1  24185  abelthlem3  24187  abelthlem6  24190  logtayl  24406  leibpi  24669  dfef2  24697  emcllem4  24725  emcllem6  24727  emcllem7  24728  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamcvg2  24781  basellem6  24812  sqff1o  24908  dchrptlem2  24990  dchrptlem3  24991  2lgslem1  25119  dchrisumlem3  25180  padicfval  25305  padicabvf  25320  istrkg2ld  25359  ishlg  25497  mirval  25550  ishpg  25651  lmif  25677  islmib  25679  axlowdim  25841  crctcshlem3  26711  wlkisowwlkupgr  26766  nmoofval  27617  htthlem  27774  pjhfval  28255  pjmfn  28574  hosmval  28594  hommval  28595  hodmval  28596  hfsmval  28597  hfmmval  28598  eigvalfval  28756  brafval  28802  kbfval  28811  rnbra  28966  bra11  28967  padct  29497  fpwrelmap  29508  sgnsv  29727  locfinreflem  29907  ordtconnlem1  29970  xrhval  30062  sigapildsys  30225  sxbrsigalem2  30348  eulerpart  30444  dstfrvclim1  30539  ballotlemfval  30551  ballotlemsval  30570  signstfv  30640  vtsval  30715  cvmliftlem5  31271  mvrsval  31402  mrsubffval  31404  mrsubfval  31405  msubffval  31420  msubfval  31421  msubrn  31426  msubco  31428  mvhfval  31430  msrfval  31434  msubvrs  31457  circum  31568  divcnvlin  31618  climlec3  31619  faclimlem2  31630  faclim2  31634  knoppcnlem1  32483  knoppcnlem6  32488  knoppcnlem7  32489  cnndvlem2  32529  ptrest  33408  poimirlem17  33426  poimirlem20  33429  voliunnfl  33453  volsupnfl  33454  upixp  33524  sdclem2  33538  fdc  33541  lmclim2  33554  geomcau  33555  rrncmslem  33631  lkrfval  34374  pmapfval  35042  pclfvalN  35175  polfvalN  35190  watfvalN  35278  ldilfset  35394  ltrnfset  35403  dilfsetN  35439  trnfsetN  35442  trlfset  35447  trlset  35448  tgrpfset  36032  tendofset  36046  tendopl  36064  tendoi  36082  erngfset  36087  erngfset-rN  36095  dvafset  36292  diaffval  36319  dvhfset  36369  docaffvalN  36410  docafvalN  36411  djaffvalN  36422  dibffval  36429  dibfval  36430  dibopelvalN  36432  dibopelval2  36434  dibelval3  36436  dibn0  36442  dib0  36453  diblsmopel  36460  dicffval  36463  dicn0  36481  dihffval  36519  dihfval  36520  dihopelvalcpre  36537  dihatlat  36623  dihpN  36625  dochffval  36638  dochfval  36639  djhffval  36685  lcfrlem8  36838  lcfrlem9  36839  lcdfval  36877  mapdffval  36915  mapdfval  36916  hvmapffval  37047  hvmapfval  37048  hvmapval  37049  hdmap1ffval  37085  hdmap1fval  37086  hdmapffval  37118  hdmapfval  37119  hgmapffval  37177  hgmapfval  37178  hlhilset  37226  mzpincl  37297  dfac11  37632  dfac21  37636  hbtlem1  37693  hbtlem7  37695  rgspnval  37738  fsovd  38302  dvgrat  38511  radcnvrat  38513  hashnzfzclim  38521  uzmptshftfval  38545  dvradcnv2  38546  binomcxplemrat  38549  binomcxplemcvg  38553  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  addrval  38670  subrval  38671  mulvval  38672  fmuldfeqlem1  39814  fmuldfeq  39815  clim1fr1  39833  climexp  39837  climneg  39842  climdivf  39844  divcnvg  39859  expfac  39889  climresmpt  39891  climsubmpt  39892  limsupval4  40026  climliminflimsupd  40033  liminfreuzlem  40034  liminfltlem  40036  dvsinax  40127  dvcosax  40141  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  stoweidlem59  40276  wallispilem5  40286  wallispi  40287  stirlinglem1  40291  stirlinglem8  40298  stirlinglem14  40304  stirlinglem15  40305  dirkerval  40308  fourierdlem71  40394  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  etransclem48  40499  salgensscntex  40562  sge0tsms  40597  nnfoctbdjlem  40672  isomenndlem  40744  ovnval  40755  ovncvrrp  40778  ovnsubaddlem1  40784  hsphoif  40790  hsphoival  40793  ovnhoilem2  40816  hoidifhspval  40822  ovncvr2  40825  hspmbllem2  40841  vonioolem1  40894  smfpimcclem  41013  smflimsuplem1  41026  smflimsuplem4  41029  smflimsuplem7  41032  smfliminflem  41036  irinitoringc  42069  aacllem  42547