Theorem mptex 6390

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 6389. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.)

Hypothesis

Ref	Expression
mptex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
mptex	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem mptex

Step	Hyp	Ref	Expression
1		mptex.1	. 2 ⊢ 𝐴 ∈ V
2		mptexg 6389	. 2 ⊢ (𝐴 ∈ V → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173   ↦ cmpt 4643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812

This theorem is referenced by:  mptrabex  6392  mptrabexOLD  6393  eufnfv  6395  fvresex  7032  abrexex  7033  ofmres  7055  noinfep  8440  cantnffval  8443  cnfcomlem  8479  cnfcom3clem  8485  fseqenlem1  8730  dfacacn  8846  dfac12lem1  8848  infmap2  8923  ackbij2lem2  8945  ackbij2lem3  8946  fin23lem32  9049  konigthlem  9269  wunex2  9439  wuncval2  9448  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  mptnn0fsupp  12659  ccatfn  13210  ccatfval  13211  swrdval  13269  swrd00  13270  swrd0  13286  revval  13360  repsundef  13369  climmpt  14150  climle  14218  iserabs  14388  isumshft  14410  divcnvshft  14426  supcvg  14427  trireciplem  14433  expcnv  14435  explecnv  14436  geolim  14440  geo2lim  14445  cvgrat  14454  mertenslem2  14456  eftlub  14678  rpnnen2lem1  14782  rpnnen2lem2  14783  1arithlem1  15465  1arith  15469  vdwapval  15515  vdwlem6  15528  vdwlem9  15531  restfn  15908  cidfval  16160  cidffn  16162  idfu2nd  16360  idfu1st  16362  idfucl  16364  fucco  16445  homafval  16502  idafval  16530  prf1  16663  prf2fval  16664  prfcl  16666  prf1st  16667  prf2nd  16668  curf1fval  16687  curf11  16689  curf12  16690  curf1cl  16691  curf2  16692  curfcl  16695  hof2val  16719  yonedalem3a  16737  yonedalem4a  16738  yonedalem4b  16739  yonedalem4c  16740  yonedalem3  16743  yonedainv  16744  lubfval  16801  glbfval  16814  grpinvfval  17283  grplactfval  17339  cntzfval  17576  psgnfval  17743  odfval  17775  sylow1lem2  17837  sylow2blem1  17858  sylow2blem2  17859  sylow3lem1  17865  sylow3lem6  17870  pj1fval  17930  vrgpfval  18002  lspfval  18794  sraval  18997  aspval  19149  asclfval  19155  psrmulfval  19206  psrass1  19226  mvrval  19242  mplmon  19284  mplcoe1  19286  evlslem2  19333  mpfrcl  19339  evlsval  19340  evlsvar  19344  mpfind  19357  coe1fval  19396  psropprmul  19429  coe1mul2  19460  ply1coe  19487  evls1fval  19505  evls1val  19506  evl1fval  19513  evl1val  19514  zrhval2  19676  submafval  20204  mdetfval  20211  madufval  20262  minmar1fval  20271  pmatcollpw2lem  20401  pm2mpval  20419  1stcfb  21058  ptbasfi  21194  dfac14  21231  fmval  21557  fmf  21559  flffval  21603  fcfval  21647  cnextval  21675  met1stc  22136  pcoval  22619  iscmet3lem3  22896  mbflimsup  23239  mbflim  23241  itg1climres  23287  mbfi1fseqlem2  23289  mbfi1fseqlem4  23291  mbfi1fseqlem6  23293  mbfi1flimlem  23295  mbfmullem2  23297  itg2monolem1  23323  itg2addlem  23331  itg2cnlem1  23334  cpnfval  23501  mdegfval  23626  ig1pval  23736  elply  23755  plyeq0lem  23770  plypf1  23772  geolim3  23898  ulmuni  23950  ulmcau  23953  ulmdvlem1  23958  ulmdvlem3  23960  mbfulm  23964  itgulm  23966  pserval  23968  dvradcnv  23979  pserdvlem2  23986  abelthlem1  23989  abelthlem3  23991  abelthlem6  23994  logtayl  24206  leibpi  24469  dfef2  24497  emcllem4  24525  emcllem6  24527  emcllem7  24528  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamcvg2  24581  basellem6  24612  sqff1o  24708  dchrptlem2  24790  dchrptlem3  24791  2lgslem1  24919  dchrisumlem3  24980  padicfval  25105  padicabvf  25120  istrkg2ld  25159  ishlg  25297  mirval  25350  ishpg  25451  lmif  25477  islmib  25479  axlowdim  25641  wwlkn  26210  clwwlkn  26295  clwwlknprop  26300  eupatrl  26495  numclwlk1lem2  26624  nmoofval  27001  htthlem  27158  pjhfval  27639  pjmfn  27958  hosmval  27978  hommval  27979  hodmval  27980  hfsmval  27981  hfmmval  27982  eigvalfval  28140  brafval  28186  kbfval  28195  rnbra  28350  bra11  28351  padct  28885  fpwrelmap  28896  sgnsv  29058  locfinreflem  29235  ordtconlem1  29298  xrhval  29390  sigapildsys  29552  sxbrsigalem2  29675  eulerpart  29771  dstfrvclim1  29866  ballotlemfval  29878  ballotlemsval  29897  signstfv  29966  cvmliftlem5  30525  mvrsval  30656  mrsubffval  30658  mrsubfval  30659  msubffval  30674  msubfval  30675  msubrn  30680  msubco  30682  mvhfval  30684  msrfval  30688  msubvrs  30711  circum  30822  divcnvlin  30871  climlec3  30872  faclimlem2  30883  faclim2  30887  knoppcnlem1  31653  knoppcnlem6  31658  knoppcnlem7  31659  cnndvlem2  31699  ptrest  32578  poimirlem17  32596  poimirlem20  32599  voliunnfl  32623  volsupnfl  32624  upixp  32694  sdclem2  32708  fdc  32711  lmclim2  32724  geomcau  32725  rrncmslem  32801  lkrfval  33392  pmapfval  34060  pclfvalN  34193  polfvalN  34208  watfvalN  34296  ldilfset  34412  ltrnfset  34421  dilfsetN  34457  trnfsetN  34460  trlfset  34465  trlset  34466  tgrpfset  35050  tendofset  35064  tendopl  35082  tendoi  35100  erngfset  35105  erngfset-rN  35113  dvafset  35310  diaffval  35337  dvhfset  35387  docaffvalN  35428  docafvalN  35429  djaffvalN  35440  dibffval  35447  dibfval  35448  dibopelvalN  35450  dibopelval2  35452  dibelval3  35454  dibn0  35460  dib0  35471  diblsmopel  35478  dicffval  35481  dicn0  35499  dihffval  35537  dihfval  35538  dihopelvalcpre  35555  dihatlat  35641  dihpN  35643  dochffval  35656  dochfval  35657  djhffval  35703  lcfrlem8  35856  lcfrlem9  35857  lcdfval  35895  mapdffval  35933  mapdfval  35934  hvmapffval  36065  hvmapfval  36066  hvmapval  36067  hdmap1ffval  36103  hdmap1fval  36104  hdmapffval  36136  hdmapfval  36137  hgmapffval  36195  hgmapfval  36196  hlhilset  36244  mzpincl  36315  dfac11  36650  dfac21  36654  hbtlem1  36712  hbtlem7  36714  rgspnval  36757  fsovd  37322  dvgrat  37533  radcnvrat  37535  hashnzfzclim  37543  uzmptshftfval  37567  dvradcnv2  37568  binomcxplemrat  37571  binomcxplemcvg  37575  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  addrval  37691  subrval  37692  mulvval  37693  fmuldfeqlem1  38649  fmuldfeq  38650  clim1fr1  38668  climexp  38672  climneg  38677  climdivf  38679  divcnvg  38694  expfac  38724  climresmpt  38726  climsubmpt  38727  dvsinax  38801  dvcosax  38816  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  stoweidlem59  38952  wallispilem5  38962  wallispi  38963  stirlinglem1  38967  stirlinglem8  38974  stirlinglem14  38980  stirlinglem15  38981  dirkerval  38984  fourierdlem71  39070  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  etransclem48  39175  salgensscntex  39238  sge0tsms  39273  nnfoctbdjlem  39348  isomenndlem  39420  ovnval  39431  ovncvrrp  39454  ovnsubaddlem1  39460  hsphoif  39466  hsphoival  39469  ovnhoilem2  39492  hoidifhspval  39498  ovncvr2  39501  hspmbllem2  39517  vonioolem1  39571  crctcshlem3  41022  1wlkisowwlkupgr  41077  av-numclwlk1lem2  41527  irinitoringc  41861  aacllem  42356