Theorem mptex 6977

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

Syntax hints:   ∈ wcel 2111  Vcvv 3409   ↦ cmpt 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343

This theorem is referenced by:  mptrabex  6979  mptfvmpt  6982  eufnfv  6983  fvresex  7665  ofmres  7689  noinfep  9156  cantnffval  9159  cnfcomlem  9195  cnfcom3clem  9201  fseqenlem1  9484  dfacacn  9601  dfac12lem1  9603  infmap2  9678  ackbij2lem2  9700  ackbij2lem3  9701  fin23lem32  9804  konigthlem  10028  wunex2  10198  wuncval2  10207  rpnnen1lem1  12418  rpnnen1lem3  12419  rpnnen1lem5  12421  mptnn0fsupp  13414  ccatfn  13971  ccatfval  13972  swrdval  14052  swrd00  14053  swrd0  14067  revval  14169  repsundef  14180  climmpt  14976  climle  15044  iserabs  15218  isumshft  15242  divcnvshft  15258  supcvg  15259  trireciplem  15265  expcnv  15267  explecnv  15268  geolim  15274  geo2lim  15279  cvgrat  15287  mertenslem2  15289  eftlub  15510  rpnnen2lem1  15615  rpnnen2lem2  15616  1arithlem1  16314  1arith  16318  vdwapval  16364  vdwlem6  16377  vdwlem9  16380  restfn  16756  cidffn  17007  idfu2nd  17206  idfu1st  17208  idfucl  17210  fucco  17291  homafval  17355  prf1  17516  prf2fval  17517  prfcl  17519  prf1st  17520  prf2nd  17521  curf1fval  17540  curf11  17542  curf12  17543  curf1cl  17544  curf2  17545  curfcl  17548  hof2val  17572  yonedalem3a  17590  yonedalem4a  17591  yonedalem4b  17592  yonedalem4c  17593  yonedalem3  17596  yonedainv  17597  lubfval  17654  glbfval  17667  smndex1gbas  18133  smndex1gid  18134  smndex1igid  18135  smndex1mnd  18141  smndex1id  18142  smndex1n0mnd  18143  smndex2dbas  18145  smndex2hbas  18147  cntzfval  18517  psgnfval  18695  sylow1lem2  18791  sylow2blem1  18812  sylow2blem2  18813  sylow3lem1  18819  sylow3lem6  18824  pj1fval  18887  vrgpfval  18959  lspfval  19813  sraval  20016  zrhval2  20278  aspval  20635  psrmulfval  20713  psrass1  20733  mvrval  20749  mplmon  20795  mplcoe1  20797  evlslem2  20842  mpfrcl  20848  evlsval  20849  evlsvar  20853  mpfind  20870  mhpfval  20882  coe1fval  20929  psropprmul  20962  coe1mul2  20993  ply1coe  21020  evls1fval  21038  evls1val  21039  evl1fval  21047  evl1val  21048  submafval  21279  mdetfval  21286  madufval  21337  minmar1fval  21346  pmatcollpw2lem  21477  pm2mpval  21495  1stcfb  22145  ptbasfi  22281  dfac14  22318  fmval  22643  fmf  22645  flffval  22689  fcfval  22733  cnextval  22761  met1stc  23223  pcoval  23712  iscmet3lem3  23990  rrxsca  24096  mbflimsup  24366  mbflim  24368  itg1climres  24414  mbfi1fseqlem2  24416  mbfi1fseqlem4  24418  mbfi1fseqlem6  24420  mbfi1flimlem  24422  mbfmullem2  24424  itg2monolem1  24450  itg2addlem  24458  itg2cnlem1  24461  cpnfval  24631  mdegfval  24762  elply  24891  plyeq0lem  24906  plypf1  24908  geolim3  25034  ulmuni  25086  ulmcau  25089  ulmdvlem1  25094  ulmdvlem3  25096  mbfulm  25100  itgulm  25102  pserval  25104  dvradcnv  25115  pserdvlem2  25122  abelthlem1  25125  abelthlem3  25127  abelthlem6  25130  logtayl  25350  leibpi  25627  dfef2  25655  emcllem4  25683  emcllem6  25685  emcllem7  25686  lgamgulmlem5  25717  lgamgulmlem6  25718  lgamcvg2  25739  basellem6  25770  sqff1o  25866  dchrptlem2  25948  dchrptlem3  25949  2lgslem1  26077  dchrisumlem3  26174  padicfval  26299  padicabvf  26314  istrkg2ld  26353  mirval  26548  ishpg  26652  lmif  26678  islmib  26680  axlowdim  26854  crctcshlem3  27704  nmoofval  28644  pjhfval  29278  pjmfn  29597  hosmval  29617  hommval  29618  hodmval  29619  hfsmval  29620  hfmmval  29621  eigvalfval  29779  brafval  29825  kbfval  29834  rnbra  29989  bra11  29990  padct  30578  fpwrelmap  30592  qusima  31115  nsgmgc  31118  nsgqusf1o  31122  idlsrgtset  31174  locfinreflem  31311  rspectopn  31338  zarcmplem  31352  ordtconnlem1  31395  xrhval  31487  sigapildsys  31649  sxbrsigalem2  31772  eulerpart  31868  dstfrvclim1  31963  ballotlemfval  31975  ballotlemsval  31994  signstfv  32061  vtsval  32136  cvmliftlem5  32767  mrsubffval  32985  mrsubfval  32986  msubffval  33001  msubfval  33002  msubrn  33007  msubco  33009  msubvrs  33038  circum  33148  divcnvlin  33213  climlec3  33214  faclimlem2  33225  faclim2  33229  knoppcnlem1  34222  knoppcnlem6  34227  knoppcnlem7  34228  cnndvlem2  34267  bj-endval  35009  ptrest  35336  poimirlem17  35354  poimirlem20  35357  voliunnfl  35381  volsupnfl  35382  upixp  35447  sdclem2  35460  fdc  35463  lmclim2  35476  geomcau  35477  rrncmslem  35550  pclfvalN  37465  polfvalN  37480  trlset  37737  tendopl  38352  docafvalN  38698  dibfval  38717  dibopelvalN  38719  dibopelval2  38721  dibelval3  38723  dibn0  38729  dib0  38740  diblsmopel  38747  dicn0  38768  dihopelvalcpre  38824  dihatlat  38910  dihpN  38912  dochfval  38926  lcfrlem9  39126  hvmapfval  39335  hvmapval  39336  hdmap1fval  39372  hlhilset  39510  evlsbagval  39780  mhphf  39790  mzpincl  40048  dfac11  40379  dfac21  40383  hbtlem1  40440  hbtlem7  40442  rgspnval  40485  fsovd  41082  mnringmulrcld  41309  dvgrat  41389  radcnvrat  41391  hashnzfzclim  41399  uzmptshftfval  41423  dvradcnv2  41424  binomcxplemrat  41427  binomcxplemcvg  41431  binomcxplemdvsum  41432  binomcxplemnotnn0  41433  addrval  41543  subrval  41544  mulvval  41545  fmuldfeqlem1  42590  fmuldfeq  42591  clim1fr1  42609  climexp  42613  climneg  42618  climdivf  42620  divcnvg  42635  expfac  42665  climresmpt  42667  climsubmpt  42668  limsupval4  42802  climliminflimsupd  42809  liminfreuzlem  42810  liminfltlem  42812  liminfpnfuz  42824  dvsinax  42921  dvcosax  42934  ioodvbdlimc1lem2  42940  ioodvbdlimc2lem  42942  dvnprodlem1  42954  dvnprodlem2  42955  dvnprodlem3  42956  stoweidlem59  43067  wallispilem5  43077  wallispi  43078  stirlinglem1  43082  stirlinglem8  43089  stirlinglem14  43095  stirlinglem15  43096  dirkerval  43099  fourierdlem71  43185  fourierdlem103  43217  fourierdlem104  43218  fourierdlem112  43226  etransclem48  43290  salgensscntex  43350  sge0tsms  43385  nnfoctbdjlem  43460  isomenndlem  43535  ovnval  43546  ovncvrrp  43569  ovnsubaddlem1  43575  hsphoif  43581  hsphoival  43584  ovnhoilem2  43607  hoidifhspval  43613  ovncvr2  43616  hspmbllem2  43632  vonioolem1  43685  smfpimcclem  43804  smflimsuplem1  43817  smflimsuplem4  43820  smflimsuplem7  43823  smfliminflem  43827  isomuspgrlem2  44718  irinitoringc  45060  1aryenef  45424  2aryenef  45435  itcovalpclem2  45450  itcovalt2lem2  45455  ackvalsuc1mpt  45457  ackval0  45459  aacllem  45720