Theorem mptex 7179

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442   ↦ cmpt 5181

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508

This theorem is referenced by:  mptrabex  7181  mptfvmpt  7184  eufnfv  7185  fvresex  7914  ofmres  7938  noinfep  9581  cantnffval  9584  cnfcomlem  9620  cnfcom3clem  9626  ssttrcl  9636  ttrcltr  9637  ttrclselem2  9647  fseqenlem1  9946  dfacacn  10064  dfac12lem1  10066  infmap2  10139  ackbij2lem2  10161  ackbij2lem3  10162  fin23lem32  10266  konigthlem  10491  wunex2  10661  wuncval2  10670  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  mptnn0fsupp  13932  ccatfn  14507  ccatfval  14508  swrdval  14579  swrd00  14580  swrd0  14594  revval  14695  repsundef  14706  climmpt  15506  climle  15575  iserabs  15750  isumshft  15774  divcnvshft  15790  supcvg  15791  trireciplem  15797  expcnv  15799  explecnv  15800  geolim  15805  geo2lim  15810  cvgrat  15818  mertenslem2  15820  eftlub  16046  rpnnen2lem1  16151  rpnnen2lem2  16152  1arithlem1  16863  1arith  16867  vdwapval  16913  vdwlem6  16926  vdwlem9  16929  restfn  17356  cidffn  17613  idfu2nd  17813  idfu1st  17815  idfucl  17817  fucco  17901  homafval  17965  prf1  18135  prf2fval  18136  prfcl  18138  prf1st  18139  prf2nd  18140  curf1fval  18159  curf11  18161  curf12  18162  curf1cl  18163  curf2  18164  curfcl  18167  hof2val  18191  yonedalem3a  18209  yonedalem4a  18210  yonedalem4b  18211  yonedalem4c  18212  yonedalem3  18215  yonedainv  18216  lubfval  18283  glbfval  18296  smndex1gbas  18839  smndex1gid  18840  smndex1igid  18841  smndex1mnd  18847  smndex1id  18848  smndex1n0mnd  18849  smndex2dbas  18851  smndex2hbas  18853  cntzfval  19261  psgnfval  19441  sylow1lem2  19540  sylow2blem1  19561  sylow2blem2  19562  sylow3lem1  19568  sylow3lem6  19573  pj1fval  19635  vrgpfval  19707  rgspnval  20557  lspfval  20936  sraval  21139  irinitoringc  21446  zrhval2  21475  aspval  21840  psrmulfval  21911  psrass1  21931  mvrval  21949  mplmon  22002  mplcoe1  22004  evlslem2  22046  mpfrcl  22052  evlsval  22053  evlsvvvallem2  22059  evlsvvval  22060  evlsvar  22062  mpfind  22082  mhpfval  22093  psdval  22114  psdmul  22121  coe1fval  22158  psropprmul  22190  coe1mul2  22223  ply1coe  22254  evls1fval  22275  evls1val  22276  evl1fval  22284  evl1val  22285  submafval  22535  mdetfval  22542  madufval  22593  minmar1fval  22602  pmatcollpw2lem  22733  pm2mpval  22751  1stcfb  23401  ptbasfi  23537  dfac14  23574  fmval  23899  fmf  23901  flffval  23945  fcfval  23989  cnextval  24017  met1stc  24477  pcoval  24979  iscmet3lem3  25258  rrxsca  25364  mbflimsup  25635  mbflim  25637  itg1climres  25683  mbfi1fseqlem2  25685  mbfi1fseqlem4  25687  mbfi1fseqlem6  25689  mbfi1flimlem  25691  mbfmullem2  25693  itg2monolem1  25719  itg2addlem  25727  itg2cnlem1  25730  cpnfval  25902  mdegfval  26035  elply  26168  plyeq0lem  26183  plypf1  26185  geolim3  26315  ulmuni  26369  ulmcau  26372  ulmdvlem1  26377  ulmdvlem3  26379  mbfulm  26383  itgulm  26385  pserval  26387  dvradcnv  26398  pserdvlem2  26406  abelthlem1  26409  abelthlem3  26411  abelthlem6  26414  logtayl  26637  leibpi  26920  dfef2  26949  emcllem4  26977  emcllem6  26979  emcllem7  26980  lgamgulmlem5  27011  lgamgulmlem6  27012  lgamcvg2  27033  basellem6  27064  sqff1o  27160  dchrptlem2  27244  dchrptlem3  27245  2lgslem1  27373  dchrisumlem3  27470  padicfval  27595  padicabvf  27610  istrkg2ld  28544  mirval  28739  ishpg  28843  lmif  28869  islmib  28871  axlowdim  29046  crctcshlem3  29904  nmoofval  30849  pjhfval  31483  pjmfn  31802  hosmval  31822  hommval  31823  hodmval  31824  hfsmval  31825  hfmmval  31826  eigvalfval  31984  brafval  32030  kbfval  32039  rnbra  32194  bra11  32195  padct  32807  fpwrelmap  32822  qusima  33500  nsgmgc  33504  nsgqusf1o  33508  idlsrgtset  33600  extvfval  33708  mplvrpmga  33721  esplyval  33738  locfinreflem  34017  rspectopn  34044  zarcmplem  34058  ordtconnlem1  34101  xrhval  34195  sigapildsys  34339  sxbrsigalem2  34463  eulerpart  34559  dstfrvclim1  34655  ballotlemfval  34667  ballotlemsval  34686  signstfv  34740  vtsval  34814  fineqvnttrclse  35299  cvmliftlem5  35502  mrsubffval  35720  mrsubfval  35721  msubffval  35736  msubfval  35737  msubrn  35742  msubco  35744  msubvrs  35773  circum  35887  divcnvlin  35946  climlec3  35947  faclimlem2  35957  faclim2  35961  knoppcnlem1  36712  knoppcnlem6  36717  knoppcnlem7  36718  cnndvlem2  36757  bj-endval  37564  ptrest  37864  poimirlem17  37882  poimirlem20  37885  voliunnfl  37909  volsupnfl  37910  upixp  37974  sdclem2  37987  fdc  37990  lmclim2  38003  geomcau  38004  rrncmslem  38077  pclfvalN  40259  polfvalN  40274  trlset  40531  tendopl  41146  docafvalN  41492  dibfval  41511  dibopelvalN  41513  dibopelval2  41515  dibelval3  41517  dibn0  41523  dib0  41534  diblsmopel  41541  dicn0  41562  dihopelvalcpre  41618  dihatlat  41704  dihpN  41706  dochfval  41720  lcfrlem9  41920  hvmapfval  42129  hvmapval  42130  hdmap1fval  42166  hlhilset  42304  sticksstones10  42519  sticksstones12a  42521  aks6d1c6isolem2  42539  selvvvval  42937  evlselv  42939  prjcrvfval  42983  mzpincl  43085  dfac11  43413  dfac21  43417  hbtlem1  43474  hbtlem7  43476  fsovd  44358  mnringmulrcld  44578  dvgrat  44662  radcnvrat  44664  hashnzfzclim  44672  uzmptshftfval  44696  dvradcnv2  44697  binomcxplemrat  44700  binomcxplemcvg  44704  binomcxplemdvsum  44705  binomcxplemnotnn0  44706  addrval  44815  subrval  44816  mulvval  44817  fmuldfeqlem1  45936  fmuldfeq  45937  clim1fr1  45955  climexp  45959  climneg  45964  climdivf  45966  divcnvg  45981  expfac  46009  climresmpt  46011  climsubmpt  46012  limsupval4  46146  climliminflimsupd  46153  liminfreuzlem  46154  liminfltlem  46156  liminfpnfuz  46168  dvsinax  46265  dvcosax  46278  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  dvnprodlem1  46298  dvnprodlem2  46299  dvnprodlem3  46300  stoweidlem59  46411  wallispilem5  46421  wallispi  46422  stirlinglem1  46426  stirlinglem8  46433  stirlinglem14  46439  stirlinglem15  46440  dirkerval  46443  fourierdlem71  46529  fourierdlem103  46561  fourierdlem104  46562  fourierdlem112  46570  etransclem48  46634  salgensscntex  46696  sge0tsms  46732  nnfoctbdjlem  46807  isomenndlem  46882  ovnval  46893  ovncvrrp  46916  ovnsubaddlem1  46922  hsphoif  46928  hsphoival  46931  ovnhoilem2  46954  hoidifhspval  46960  ovncvr2  46963  hspmbllem2  46979  vonioolem1  47032  smfpimcclem  47159  smflimsuplem1  47172  smflimsuplem4  47175  smflimsuplem7  47178  smfliminflem  47182  fsupdm  47194  smfsupdmmbllem  47196  finfdm  47198  smfinfdmmbllem  47200  cfsetsnfsetfo  47414  isuspgrim0  48248  cycldlenngric  48282  isgrtri  48297  1aryenef  48999  2aryenef  49010  itcovalpclem2  49025  itcovalt2lem2  49030  ackvalsuc1mpt  49032  ackval0  49034  cofidvala  49469  cofidval  49472  isnatd  49576  swapfelvv  49616  swapf2fvala  49617  swapf1vala  49619  swapf2fn  49621  swapf2vala  49623  tposcurf1  49652  prcofelvv  49733  reldmprcof1  49734  reldmprcof2  49735  prcof1  49741  prcof2a  49742  prcof2  49743  idfudiag1bas  49877  idfudiag1  49878  lmdfval  50002  cmdfval  50003  aacllem  50154