Theorem mptex 7225

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475   ↦ cmpt 5232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552

This theorem is referenced by:  mptrabex  7227  mptfvmpt  7230  eufnfv  7231  fvresex  7946  ofmres  7971  noinfep  9655  cantnffval  9658  cnfcomlem  9694  cnfcom3clem  9700  ssttrcl  9710  ttrcltr  9711  ttrclselem2  9721  fseqenlem1  10019  dfacacn  10136  dfac12lem1  10138  infmap2  10213  ackbij2lem2  10235  ackbij2lem3  10236  fin23lem32  10339  konigthlem  10563  wunex2  10733  wuncval2  10742  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  mptnn0fsupp  13962  ccatfn  14522  ccatfval  14523  swrdval  14593  swrd00  14594  swrd0  14608  revval  14710  repsundef  14721  climmpt  15515  climle  15584  iserabs  15761  isumshft  15785  divcnvshft  15801  supcvg  15802  trireciplem  15808  expcnv  15810  explecnv  15811  geolim  15816  geo2lim  15821  cvgrat  15829  mertenslem2  15831  eftlub  16052  rpnnen2lem1  16157  rpnnen2lem2  16158  1arithlem1  16856  1arith  16860  vdwapval  16906  vdwlem6  16919  vdwlem9  16922  restfn  17370  cidffn  17622  idfu2nd  17827  idfu1st  17829  idfucl  17831  fucco  17915  homafval  17979  prf1  18152  prf2fval  18153  prfcl  18155  prf1st  18156  prf2nd  18157  curf1fval  18177  curf11  18179  curf12  18180  curf1cl  18181  curf2  18182  curfcl  18185  hof2val  18209  yonedalem3a  18227  yonedalem4a  18228  yonedalem4b  18229  yonedalem4c  18230  yonedalem3  18233  yonedainv  18234  lubfval  18303  glbfval  18316  smndex1gbas  18783  smndex1gid  18784  smndex1igid  18785  smndex1mnd  18791  smndex1id  18792  smndex1n0mnd  18793  smndex2dbas  18795  smndex2hbas  18797  cntzfval  19184  psgnfval  19368  sylow1lem2  19467  sylow2blem1  19488  sylow2blem2  19489  sylow3lem1  19495  sylow3lem6  19500  pj1fval  19562  vrgpfval  19634  lspfval  20584  sraval  20789  zrhval2  21058  aspval  21427  psrmulfval  21504  psrass1  21525  mvrval  21541  mplmon  21590  mplcoe1  21592  evlslem2  21642  mpfrcl  21648  evlsval  21649  evlsvar  21653  mpfind  21670  mhpfval  21682  coe1fval  21729  psropprmul  21760  coe1mul2  21791  ply1coe  21820  evls1fval  21838  evls1val  21839  evl1fval  21847  evl1val  21848  submafval  22081  mdetfval  22088  madufval  22139  minmar1fval  22148  pmatcollpw2lem  22279  pm2mpval  22297  1stcfb  22949  ptbasfi  23085  dfac14  23122  fmval  23447  fmf  23449  flffval  23493  fcfval  23537  cnextval  23565  met1stc  24030  pcoval  24527  iscmet3lem3  24807  rrxsca  24913  mbflimsup  25183  mbflim  25185  itg1climres  25232  mbfi1fseqlem2  25234  mbfi1fseqlem4  25236  mbfi1fseqlem6  25238  mbfi1flimlem  25240  mbfmullem2  25242  itg2monolem1  25268  itg2addlem  25276  itg2cnlem1  25279  cpnfval  25449  mdegfval  25580  elply  25709  plyeq0lem  25724  plypf1  25726  geolim3  25852  ulmuni  25904  ulmcau  25907  ulmdvlem1  25912  ulmdvlem3  25914  mbfulm  25918  itgulm  25920  pserval  25922  dvradcnv  25933  pserdvlem2  25940  abelthlem1  25943  abelthlem3  25945  abelthlem6  25948  logtayl  26168  leibpi  26447  dfef2  26475  emcllem4  26503  emcllem6  26505  emcllem7  26506  lgamgulmlem5  26537  lgamgulmlem6  26538  lgamcvg2  26559  basellem6  26590  sqff1o  26686  dchrptlem2  26768  dchrptlem3  26769  2lgslem1  26897  dchrisumlem3  26994  padicfval  27119  padicabvf  27134  istrkg2ld  27711  mirval  27906  ishpg  28010  lmif  28036  islmib  28038  axlowdim  28219  crctcshlem3  29073  nmoofval  30015  pjhfval  30649  pjmfn  30968  hosmval  30988  hommval  30989  hodmval  30990  hfsmval  30991  hfmmval  30992  eigvalfval  31150  brafval  31196  kbfval  31205  rnbra  31360  bra11  31361  padct  31944  fpwrelmap  31958  qusima  32519  nsgmgc  32523  nsgqusf1o  32527  idlsrgtset  32622  locfinreflem  32820  rspectopn  32847  zarcmplem  32861  ordtconnlem1  32904  xrhval  32998  sigapildsys  33160  sxbrsigalem2  33285  eulerpart  33381  dstfrvclim1  33476  ballotlemfval  33488  ballotlemsval  33507  signstfv  33574  vtsval  33649  cvmliftlem5  34280  mrsubffval  34498  mrsubfval  34499  msubffval  34514  msubfval  34515  msubrn  34520  msubco  34522  msubvrs  34551  circum  34659  divcnvlin  34702  climlec3  34703  faclimlem2  34714  faclim2  34718  knoppcnlem1  35369  knoppcnlem6  35374  knoppcnlem7  35375  cnndvlem2  35414  bj-endval  36196  ptrest  36487  poimirlem17  36505  poimirlem20  36508  voliunnfl  36532  volsupnfl  36533  upixp  36597  sdclem2  36610  fdc  36613  lmclim2  36626  geomcau  36627  rrncmslem  36700  pclfvalN  38760  polfvalN  38775  trlset  39032  tendopl  39647  docafvalN  39993  dibfval  40012  dibopelvalN  40014  dibopelval2  40016  dibelval3  40018  dibn0  40024  dib0  40035  diblsmopel  40042  dicn0  40063  dihopelvalcpre  40119  dihatlat  40205  dihpN  40207  dochfval  40221  lcfrlem9  40421  hvmapfval  40630  hvmapval  40631  hdmap1fval  40667  hlhilset  40805  sticksstones10  40971  sticksstones12a  40973  evlsvvvallem2  41134  evlsvvval  41135  selvvvval  41157  evlselv  41159  prjcrvfval  41373  mzpincl  41472  dfac11  41804  dfac21  41808  hbtlem1  41865  hbtlem7  41867  rgspnval  41910  fsovd  42759  mnringmulrcld  42987  dvgrat  43071  radcnvrat  43073  hashnzfzclim  43081  uzmptshftfval  43105  dvradcnv2  43106  binomcxplemrat  43109  binomcxplemcvg  43113  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  addrval  43225  subrval  43226  mulvval  43227  fmuldfeqlem1  44298  fmuldfeq  44299  clim1fr1  44317  climexp  44321  climneg  44326  climdivf  44328  divcnvg  44343  expfac  44373  climresmpt  44375  climsubmpt  44376  limsupval4  44510  climliminflimsupd  44517  liminfreuzlem  44518  liminfltlem  44520  liminfpnfuz  44532  dvsinax  44629  dvcosax  44642  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnprodlem1  44662  dvnprodlem2  44663  dvnprodlem3  44664  stoweidlem59  44775  wallispilem5  44785  wallispi  44786  stirlinglem1  44790  stirlinglem8  44797  stirlinglem14  44803  stirlinglem15  44804  dirkerval  44807  fourierdlem71  44893  fourierdlem103  44925  fourierdlem104  44926  fourierdlem112  44934  etransclem48  44998  salgensscntex  45060  sge0tsms  45096  nnfoctbdjlem  45171  isomenndlem  45246  ovnval  45257  ovncvrrp  45280  ovnsubaddlem1  45286  hsphoif  45292  hsphoival  45295  ovnhoilem2  45318  hoidifhspval  45324  ovncvr2  45327  hspmbllem2  45343  vonioolem1  45396  smfpimcclem  45523  smflimsuplem1  45536  smflimsuplem4  45539  smflimsuplem7  45542  smfliminflem  45546  fsupdm  45558  smfsupdmmbllem  45560  finfdm  45562  smfinfdmmbllem  45564  cfsetsnfsetfo  45770  isomuspgrlem2  46501  irinitoringc  46967  1aryenef  47331  2aryenef  47342  itcovalpclem2  47357  itcovalt2lem2  47362  ackvalsuc1mpt  47364  ackval0  47366  aacllem  47848