Theorem mptex 7242

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570

This theorem is referenced by:  mptrabex  7244  mptfvmpt  7247  eufnfv  7248  fvresex  7982  ofmres  8007  noinfep  9697  cantnffval  9700  cnfcomlem  9736  cnfcom3clem  9742  ssttrcl  9752  ttrcltr  9753  ttrclselem2  9763  fseqenlem1  10061  dfacacn  10179  dfac12lem1  10181  infmap2  10254  ackbij2lem2  10276  ackbij2lem3  10277  fin23lem32  10381  konigthlem  10605  wunex2  10775  wuncval2  10784  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem5  13020  mptnn0fsupp  14034  ccatfn  14606  ccatfval  14607  swrdval  14677  swrd00  14678  swrd0  14692  revval  14794  repsundef  14805  climmpt  15603  climle  15672  iserabs  15847  isumshft  15871  divcnvshft  15887  supcvg  15888  trireciplem  15894  expcnv  15896  explecnv  15897  geolim  15902  geo2lim  15907  cvgrat  15915  mertenslem2  15917  eftlub  16141  rpnnen2lem1  16246  rpnnen2lem2  16247  1arithlem1  16956  1arith  16960  vdwapval  17006  vdwlem6  17019  vdwlem9  17022  restfn  17470  cidffn  17722  idfu2nd  17927  idfu1st  17929  idfucl  17931  fucco  18018  homafval  18082  prf1  18255  prf2fval  18256  prfcl  18258  prf1st  18259  prf2nd  18260  curf1fval  18280  curf11  18282  curf12  18283  curf1cl  18284  curf2  18285  curfcl  18288  hof2val  18312  yonedalem3a  18330  yonedalem4a  18331  yonedalem4b  18332  yonedalem4c  18333  yonedalem3  18336  yonedainv  18337  lubfval  18407  glbfval  18420  smndex1gbas  18927  smndex1gid  18928  smndex1igid  18929  smndex1mnd  18935  smndex1id  18936  smndex1n0mnd  18937  smndex2dbas  18939  smndex2hbas  18941  cntzfval  19350  psgnfval  19532  sylow1lem2  19631  sylow2blem1  19652  sylow2blem2  19653  sylow3lem1  19659  sylow3lem6  19664  pj1fval  19726  vrgpfval  19798  rgspnval  20628  lspfval  20988  sraval  21191  irinitoringc  21507  zrhval2  21536  aspval  21910  psrmulfval  21980  psrass1  22001  mvrval  22019  mplmon  22070  mplcoe1  22072  evlslem2  22120  mpfrcl  22126  evlsval  22127  evlsvar  22131  mpfind  22148  mhpfval  22159  psdval  22180  psdmul  22187  coe1fval  22222  psropprmul  22254  coe1mul2  22287  ply1coe  22317  evls1fval  22338  evls1val  22339  evl1fval  22347  evl1val  22348  submafval  22600  mdetfval  22607  madufval  22658  minmar1fval  22667  pmatcollpw2lem  22798  pm2mpval  22816  1stcfb  23468  ptbasfi  23604  dfac14  23641  fmval  23966  fmf  23968  flffval  24012  fcfval  24056  cnextval  24084  met1stc  24549  pcoval  25057  iscmet3lem3  25337  rrxsca  25443  mbflimsup  25714  mbflim  25716  itg1climres  25763  mbfi1fseqlem2  25765  mbfi1fseqlem4  25767  mbfi1fseqlem6  25769  mbfi1flimlem  25771  mbfmullem2  25773  itg2monolem1  25799  itg2addlem  25807  itg2cnlem1  25810  cpnfval  25982  mdegfval  26115  elply  26248  plyeq0lem  26263  plypf1  26265  geolim3  26395  ulmuni  26449  ulmcau  26452  ulmdvlem1  26457  ulmdvlem3  26459  mbfulm  26463  itgulm  26465  pserval  26467  dvradcnv  26478  pserdvlem2  26486  abelthlem1  26489  abelthlem3  26491  abelthlem6  26494  logtayl  26716  leibpi  26999  dfef2  27028  emcllem4  27056  emcllem6  27058  emcllem7  27059  lgamgulmlem5  27090  lgamgulmlem6  27091  lgamcvg2  27112  basellem6  27143  sqff1o  27239  dchrptlem2  27323  dchrptlem3  27324  2lgslem1  27452  dchrisumlem3  27549  padicfval  27674  padicabvf  27689  istrkg2ld  28482  mirval  28677  ishpg  28781  lmif  28807  islmib  28809  axlowdim  28990  crctcshlem3  29848  nmoofval  30790  pjhfval  31424  pjmfn  31743  hosmval  31763  hommval  31764  hodmval  31765  hfsmval  31766  hfmmval  31767  eigvalfval  31925  brafval  31971  kbfval  31980  rnbra  32135  bra11  32136  padct  32736  fpwrelmap  32750  qusima  33415  nsgmgc  33419  nsgqusf1o  33423  idlsrgtset  33515  locfinreflem  33800  rspectopn  33827  zarcmplem  33841  ordtconnlem1  33884  xrhval  33980  sigapildsys  34142  sxbrsigalem2  34267  eulerpart  34363  dstfrvclim1  34458  ballotlemfval  34470  ballotlemsval  34489  signstfv  34556  vtsval  34630  cvmliftlem5  35273  mrsubffval  35491  mrsubfval  35492  msubffval  35507  msubfval  35508  msubrn  35513  msubco  35515  msubvrs  35544  circum  35658  divcnvlin  35712  climlec3  35713  faclimlem2  35723  faclim2  35727  knoppcnlem1  36475  knoppcnlem6  36480  knoppcnlem7  36481  cnndvlem2  36520  bj-endval  37297  ptrest  37605  poimirlem17  37623  poimirlem20  37626  voliunnfl  37650  volsupnfl  37651  upixp  37715  sdclem2  37728  fdc  37731  lmclim2  37744  geomcau  37745  rrncmslem  37818  pclfvalN  39871  polfvalN  39886  trlset  40143  tendopl  40758  docafvalN  41104  dibfval  41123  dibopelvalN  41125  dibopelval2  41127  dibelval3  41129  dibn0  41135  dib0  41146  diblsmopel  41153  dicn0  41174  dihopelvalcpre  41230  dihatlat  41316  dihpN  41318  dochfval  41332  lcfrlem9  41532  hvmapfval  41741  hvmapval  41742  hdmap1fval  41778  hlhilset  41916  sticksstones10  42136  sticksstones12a  42138  aks6d1c6isolem2  42156  evlsvvvallem2  42548  evlsvvval  42549  selvvvval  42571  evlselv  42573  prjcrvfval  42617  mzpincl  42721  dfac11  43050  dfac21  43054  hbtlem1  43111  hbtlem7  43113  fsovd  43997  mnringmulrcld  44223  dvgrat  44307  radcnvrat  44309  hashnzfzclim  44317  uzmptshftfval  44341  dvradcnv2  44342  binomcxplemrat  44345  binomcxplemcvg  44349  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  addrval  44461  subrval  44462  mulvval  44463  fmuldfeqlem1  45537  fmuldfeq  45538  clim1fr1  45556  climexp  45560  climneg  45565  climdivf  45567  divcnvg  45582  expfac  45612  climresmpt  45614  climsubmpt  45615  limsupval4  45749  climliminflimsupd  45756  liminfreuzlem  45757  liminfltlem  45759  liminfpnfuz  45771  dvsinax  45868  dvcosax  45881  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnprodlem1  45901  dvnprodlem2  45902  dvnprodlem3  45903  stoweidlem59  46014  wallispilem5  46024  wallispi  46025  stirlinglem1  46029  stirlinglem8  46036  stirlinglem14  46042  stirlinglem15  46043  dirkerval  46046  fourierdlem71  46132  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  etransclem48  46237  salgensscntex  46299  sge0tsms  46335  nnfoctbdjlem  46410  isomenndlem  46485  ovnval  46496  ovncvrrp  46519  ovnsubaddlem1  46525  hsphoif  46531  hsphoival  46534  ovnhoilem2  46557  hoidifhspval  46563  ovncvr2  46566  hspmbllem2  46582  vonioolem1  46635  smfpimcclem  46762  smflimsuplem1  46775  smflimsuplem4  46778  smflimsuplem7  46781  smfliminflem  46785  fsupdm  46797  smfsupdmmbllem  46799  finfdm  46801  smfinfdmmbllem  46803  cfsetsnfsetfo  47009  isuspgrim0  47809  isgrtri  47847  1aryenef  48494  2aryenef  48505  itcovalpclem2  48520  itcovalt2lem2  48525  ackvalsuc1mpt  48527  ackval0  48529  aacllem  49031