Theorem mptex 7081

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7079. (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 7079	. 2 ⊢ (𝐴 ∈ V → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3422   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426

This theorem is referenced by:  mptrabex  7083  mptfvmpt  7086  eufnfv  7087  fvresex  7776  ofmres  7800  noinfep  9348  cantnffval  9351  cnfcomlem  9387  cnfcom3clem  9393  fseqenlem1  9711  dfacacn  9828  dfac12lem1  9830  infmap2  9905  ackbij2lem2  9927  ackbij2lem3  9928  fin23lem32  10031  konigthlem  10255  wunex2  10425  wuncval2  10434  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  mptnn0fsupp  13645  ccatfn  14203  ccatfval  14204  swrdval  14284  swrd00  14285  swrd0  14299  revval  14401  repsundef  14412  climmpt  15208  climle  15277  iserabs  15455  isumshft  15479  divcnvshft  15495  supcvg  15496  trireciplem  15502  expcnv  15504  explecnv  15505  geolim  15510  geo2lim  15515  cvgrat  15523  mertenslem2  15525  eftlub  15746  rpnnen2lem1  15851  rpnnen2lem2  15852  1arithlem1  16552  1arith  16556  vdwapval  16602  vdwlem6  16615  vdwlem9  16618  restfn  17052  cidffn  17304  idfu2nd  17508  idfu1st  17510  idfucl  17512  fucco  17596  homafval  17660  prf1  17833  prf2fval  17834  prfcl  17836  prf1st  17837  prf2nd  17838  curf1fval  17858  curf11  17860  curf12  17861  curf1cl  17862  curf2  17863  curfcl  17866  hof2val  17890  yonedalem3a  17908  yonedalem4a  17909  yonedalem4b  17910  yonedalem4c  17911  yonedalem3  17914  yonedainv  17915  lubfval  17983  glbfval  17996  smndex1gbas  18456  smndex1gid  18457  smndex1igid  18458  smndex1mnd  18464  smndex1id  18465  smndex1n0mnd  18466  smndex2dbas  18468  smndex2hbas  18470  cntzfval  18841  psgnfval  19023  sylow1lem2  19119  sylow2blem1  19140  sylow2blem2  19141  sylow3lem1  19147  sylow3lem6  19152  pj1fval  19215  vrgpfval  19287  lspfval  20150  sraval  20353  zrhval2  20622  aspval  20987  psrmulfval  21064  psrass1  21084  mvrval  21100  mplmon  21146  mplcoe1  21148  evlslem2  21199  mpfrcl  21205  evlsval  21206  evlsvar  21210  mpfind  21227  mhpfval  21239  coe1fval  21286  psropprmul  21319  coe1mul2  21350  ply1coe  21377  evls1fval  21395  evls1val  21396  evl1fval  21404  evl1val  21405  submafval  21636  mdetfval  21643  madufval  21694  minmar1fval  21703  pmatcollpw2lem  21834  pm2mpval  21852  1stcfb  22504  ptbasfi  22640  dfac14  22677  fmval  23002  fmf  23004  flffval  23048  fcfval  23092  cnextval  23120  met1stc  23583  pcoval  24080  iscmet3lem3  24359  rrxsca  24465  mbflimsup  24735  mbflim  24737  itg1climres  24784  mbfi1fseqlem2  24786  mbfi1fseqlem4  24788  mbfi1fseqlem6  24790  mbfi1flimlem  24792  mbfmullem2  24794  itg2monolem1  24820  itg2addlem  24828  itg2cnlem1  24831  cpnfval  25001  mdegfval  25132  elply  25261  plyeq0lem  25276  plypf1  25278  geolim3  25404  ulmuni  25456  ulmcau  25459  ulmdvlem1  25464  ulmdvlem3  25466  mbfulm  25470  itgulm  25472  pserval  25474  dvradcnv  25485  pserdvlem2  25492  abelthlem1  25495  abelthlem3  25497  abelthlem6  25500  logtayl  25720  leibpi  25997  dfef2  26025  emcllem4  26053  emcllem6  26055  emcllem7  26056  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamcvg2  26109  basellem6  26140  sqff1o  26236  dchrptlem2  26318  dchrptlem3  26319  2lgslem1  26447  dchrisumlem3  26544  padicfval  26669  padicabvf  26684  istrkg2ld  26725  mirval  26920  ishpg  27024  lmif  27050  islmib  27052  axlowdim  27232  crctcshlem3  28085  nmoofval  29025  pjhfval  29659  pjmfn  29978  hosmval  29998  hommval  29999  hodmval  30000  hfsmval  30001  hfmmval  30002  eigvalfval  30160  brafval  30206  kbfval  30215  rnbra  30370  bra11  30371  padct  30956  fpwrelmap  30970  qusima  31496  nsgmgc  31499  nsgqusf1o  31503  idlsrgtset  31555  locfinreflem  31692  rspectopn  31719  zarcmplem  31733  ordtconnlem1  31776  xrhval  31868  sigapildsys  32030  sxbrsigalem2  32153  eulerpart  32249  dstfrvclim1  32344  ballotlemfval  32356  ballotlemsval  32375  signstfv  32442  vtsval  32517  cvmliftlem5  33151  mrsubffval  33369  mrsubfval  33370  msubffval  33385  msubfval  33386  msubrn  33391  msubco  33393  msubvrs  33422  circum  33532  divcnvlin  33604  climlec3  33605  faclimlem2  33616  faclim2  33620  ssttrcl  33701  ttrcltr  33702  ttrclselem2  33712  knoppcnlem1  34600  knoppcnlem6  34605  knoppcnlem7  34606  cnndvlem2  34645  bj-endval  35413  ptrest  35703  poimirlem17  35721  poimirlem20  35724  voliunnfl  35748  volsupnfl  35749  upixp  35814  sdclem2  35827  fdc  35830  lmclim2  35843  geomcau  35844  rrncmslem  35917  pclfvalN  37830  polfvalN  37845  trlset  38102  tendopl  38717  docafvalN  39063  dibfval  39082  dibopelvalN  39084  dibopelval2  39086  dibelval3  39088  dibn0  39094  dib0  39105  diblsmopel  39112  dicn0  39133  dihopelvalcpre  39189  dihatlat  39275  dihpN  39277  dochfval  39291  lcfrlem9  39491  hvmapfval  39700  hvmapval  39701  hdmap1fval  39737  hlhilset  39875  sticksstones10  40039  sticksstones12a  40041  evlsbagval  40198  mhphf  40208  mzpincl  40472  dfac11  40803  dfac21  40807  hbtlem1  40864  hbtlem7  40866  rgspnval  40909  fsovd  41505  mnringmulrcld  41735  dvgrat  41819  radcnvrat  41821  hashnzfzclim  41829  uzmptshftfval  41853  dvradcnv2  41854  binomcxplemrat  41857  binomcxplemcvg  41861  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  addrval  41973  subrval  41974  mulvval  41975  fmuldfeqlem1  43013  fmuldfeq  43014  clim1fr1  43032  climexp  43036  climneg  43041  climdivf  43043  divcnvg  43058  expfac  43088  climresmpt  43090  climsubmpt  43091  limsupval4  43225  climliminflimsupd  43232  liminfreuzlem  43233  liminfltlem  43235  liminfpnfuz  43247  dvsinax  43344  dvcosax  43357  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  stoweidlem59  43490  wallispilem5  43500  wallispi  43501  stirlinglem1  43505  stirlinglem8  43512  stirlinglem14  43518  stirlinglem15  43519  dirkerval  43522  fourierdlem71  43608  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  etransclem48  43713  salgensscntex  43773  sge0tsms  43808  nnfoctbdjlem  43883  isomenndlem  43958  ovnval  43969  ovncvrrp  43992  ovnsubaddlem1  43998  hsphoif  44004  hsphoival  44007  ovnhoilem2  44030  hoidifhspval  44036  ovncvr2  44039  hspmbllem2  44055  vonioolem1  44108  smfpimcclem  44227  smflimsuplem1  44240  smflimsuplem4  44243  smflimsuplem7  44246  smfliminflem  44250  cfsetsnfsetfo  44441  isomuspgrlem2  45173  irinitoringc  45515  1aryenef  45879  2aryenef  45890  itcovalpclem2  45905  itcovalt2lem2  45910  ackvalsuc1mpt  45912  ackval0  45914  aacllem  46391