Theorem mptex 7229

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

Syntax hints:   ∈ wcel 2099  Vcvv 3469   ↦ cmpt 5225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550

This theorem is referenced by:  mptrabex  7231  mptfvmpt  7234  eufnfv  7235  fvresex  7957  ofmres  7982  noinfep  9675  cantnffval  9678  cnfcomlem  9714  cnfcom3clem  9720  ssttrcl  9730  ttrcltr  9731  ttrclselem2  9741  fseqenlem1  10039  dfacacn  10156  dfac12lem1  10158  infmap2  10233  ackbij2lem2  10255  ackbij2lem3  10256  fin23lem32  10359  konigthlem  10583  wunex2  10753  wuncval2  10762  rpnnen1lem1  12984  rpnnen1lem3  12985  rpnnen1lem5  12987  mptnn0fsupp  13986  ccatfn  14546  ccatfval  14547  swrdval  14617  swrd00  14618  swrd0  14632  revval  14734  repsundef  14745  climmpt  15539  climle  15608  iserabs  15785  isumshft  15809  divcnvshft  15825  supcvg  15826  trireciplem  15832  expcnv  15834  explecnv  15835  geolim  15840  geo2lim  15845  cvgrat  15853  mertenslem2  15855  eftlub  16077  rpnnen2lem1  16182  rpnnen2lem2  16183  1arithlem1  16883  1arith  16887  vdwapval  16933  vdwlem6  16946  vdwlem9  16949  restfn  17397  cidffn  17649  idfu2nd  17854  idfu1st  17856  idfucl  17858  fucco  17945  homafval  18009  prf1  18182  prf2fval  18183  prfcl  18185  prf1st  18186  prf2nd  18187  curf1fval  18207  curf11  18209  curf12  18210  curf1cl  18211  curf2  18212  curfcl  18215  hof2val  18239  yonedalem3a  18257  yonedalem4a  18258  yonedalem4b  18259  yonedalem4c  18260  yonedalem3  18263  yonedainv  18264  lubfval  18333  glbfval  18346  smndex1gbas  18845  smndex1gid  18846  smndex1igid  18847  smndex1mnd  18853  smndex1id  18854  smndex1n0mnd  18855  smndex2dbas  18857  smndex2hbas  18859  cntzfval  19262  psgnfval  19446  sylow1lem2  19545  sylow2blem1  19566  sylow2blem2  19567  sylow3lem1  19573  sylow3lem6  19578  pj1fval  19640  vrgpfval  19712  lspfval  20846  sraval  21049  irinitoringc  21392  zrhval2  21421  aspval  21793  psrmulfval  21873  psrass1  21894  mvrval  21911  mplmon  21960  mplcoe1  21962  evlslem2  22012  mpfrcl  22018  evlsval  22019  evlsvar  22023  mpfind  22040  mhpfval  22050  psdmul  22077  coe1fval  22111  psropprmul  22143  coe1mul2  22175  ply1coe  22204  evls1fval  22225  evls1val  22226  evl1fval  22234  evl1val  22235  submafval  22468  mdetfval  22475  madufval  22526  minmar1fval  22535  pmatcollpw2lem  22666  pm2mpval  22684  1stcfb  23336  ptbasfi  23472  dfac14  23509  fmval  23834  fmf  23836  flffval  23880  fcfval  23924  cnextval  23952  met1stc  24417  pcoval  24925  iscmet3lem3  25205  rrxsca  25311  mbflimsup  25582  mbflim  25584  itg1climres  25631  mbfi1fseqlem2  25633  mbfi1fseqlem4  25635  mbfi1fseqlem6  25637  mbfi1flimlem  25639  mbfmullem2  25641  itg2monolem1  25667  itg2addlem  25675  itg2cnlem1  25678  cpnfval  25849  mdegfval  25985  elply  26116  plyeq0lem  26131  plypf1  26133  geolim3  26261  ulmuni  26315  ulmcau  26318  ulmdvlem1  26323  ulmdvlem3  26325  mbfulm  26329  itgulm  26331  pserval  26333  dvradcnv  26344  pserdvlem2  26352  abelthlem1  26355  abelthlem3  26357  abelthlem6  26360  logtayl  26581  leibpi  26861  dfef2  26890  emcllem4  26918  emcllem6  26920  emcllem7  26921  lgamgulmlem5  26952  lgamgulmlem6  26953  lgamcvg2  26974  basellem6  27005  sqff1o  27101  dchrptlem2  27185  dchrptlem3  27186  2lgslem1  27314  dchrisumlem3  27411  padicfval  27536  padicabvf  27551  istrkg2ld  28251  mirval  28446  ishpg  28550  lmif  28576  islmib  28578  axlowdim  28759  crctcshlem3  29617  nmoofval  30559  pjhfval  31193  pjmfn  31512  hosmval  31532  hommval  31533  hodmval  31534  hfsmval  31535  hfmmval  31536  eigvalfval  31694  brafval  31740  kbfval  31749  rnbra  31904  bra11  31905  padct  32485  fpwrelmap  32499  qusima  33058  nsgmgc  33062  nsgqusf1o  33066  idlsrgtset  33155  locfinreflem  33377  rspectopn  33404  zarcmplem  33418  ordtconnlem1  33461  xrhval  33555  sigapildsys  33717  sxbrsigalem2  33842  eulerpart  33938  dstfrvclim1  34033  ballotlemfval  34045  ballotlemsval  34064  signstfv  34131  vtsval  34205  cvmliftlem5  34835  mrsubffval  35053  mrsubfval  35054  msubffval  35069  msubfval  35070  msubrn  35075  msubco  35077  msubvrs  35106  circum  35214  divcnvlin  35263  climlec3  35264  faclimlem2  35274  faclim2  35278  knoppcnlem1  35904  knoppcnlem6  35909  knoppcnlem7  35910  cnndvlem2  35949  bj-endval  36730  ptrest  37027  poimirlem17  37045  poimirlem20  37048  voliunnfl  37072  volsupnfl  37073  upixp  37137  sdclem2  37150  fdc  37153  lmclim2  37166  geomcau  37167  rrncmslem  37240  pclfvalN  39299  polfvalN  39314  trlset  39571  tendopl  40186  docafvalN  40532  dibfval  40551  dibopelvalN  40553  dibopelval2  40555  dibelval3  40557  dibn0  40563  dib0  40574  diblsmopel  40581  dicn0  40602  dihopelvalcpre  40658  dihatlat  40744  dihpN  40746  dochfval  40760  lcfrlem9  40960  hvmapfval  41169  hvmapval  41170  hdmap1fval  41206  hlhilset  41344  sticksstones10  41559  sticksstones12a  41561  evlsvvvallem2  41717  evlsvvval  41718  selvvvval  41740  evlselv  41742  prjcrvfval  41977  mzpincl  42076  dfac11  42408  dfac21  42412  hbtlem1  42469  hbtlem7  42471  rgspnval  42514  fsovd  43361  mnringmulrcld  43588  dvgrat  43672  radcnvrat  43674  hashnzfzclim  43682  uzmptshftfval  43706  dvradcnv2  43707  binomcxplemrat  43710  binomcxplemcvg  43714  binomcxplemdvsum  43715  binomcxplemnotnn0  43716  addrval  43826  subrval  43827  mulvval  43828  fmuldfeqlem1  44893  fmuldfeq  44894  clim1fr1  44912  climexp  44916  climneg  44921  climdivf  44923  divcnvg  44938  expfac  44968  climresmpt  44970  climsubmpt  44971  limsupval4  45105  climliminflimsupd  45112  liminfreuzlem  45113  liminfltlem  45115  liminfpnfuz  45127  dvsinax  45224  dvcosax  45237  ioodvbdlimc1lem2  45243  ioodvbdlimc2lem  45245  dvnprodlem1  45257  dvnprodlem2  45258  dvnprodlem3  45259  stoweidlem59  45370  wallispilem5  45380  wallispi  45381  stirlinglem1  45385  stirlinglem8  45392  stirlinglem14  45398  stirlinglem15  45399  dirkerval  45402  fourierdlem71  45488  fourierdlem103  45520  fourierdlem104  45521  fourierdlem112  45529  etransclem48  45593  salgensscntex  45655  sge0tsms  45691  nnfoctbdjlem  45766  isomenndlem  45841  ovnval  45852  ovncvrrp  45875  ovnsubaddlem1  45881  hsphoif  45887  hsphoival  45890  ovnhoilem2  45913  hoidifhspval  45919  ovncvr2  45922  hspmbllem2  45938  vonioolem1  45991  smfpimcclem  46118  smflimsuplem1  46131  smflimsuplem4  46134  smflimsuplem7  46137  smfliminflem  46141  fsupdm  46153  smfsupdmmbllem  46155  finfdm  46157  smfinfdmmbllem  46159  cfsetsnfsetfo  46365  isuspgrim0  47093  1aryenef  47641  2aryenef  47652  itcovalpclem2  47667  itcovalt2lem2  47672  ackvalsuc1mpt  47674  ackval0  47676  aacllem  48157