Theorem mptex 7163

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438   ↦ cmpt 5176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494

This theorem is referenced by:  mptrabex  7165  mptfvmpt  7168  eufnfv  7169  fvresex  7902  ofmres  7926  noinfep  9575  cantnffval  9578  cnfcomlem  9614  cnfcom3clem  9620  ssttrcl  9630  ttrcltr  9631  ttrclselem2  9641  fseqenlem1  9937  dfacacn  10055  dfac12lem1  10057  infmap2  10130  ackbij2lem2  10152  ackbij2lem3  10153  fin23lem32  10257  konigthlem  10481  wunex2  10651  wuncval2  10660  rpnnen1lem1  12897  rpnnen1lem3  12898  rpnnen1lem5  12900  mptnn0fsupp  13922  ccatfn  14497  ccatfval  14498  swrdval  14568  swrd00  14569  swrd0  14583  revval  14684  repsundef  14695  climmpt  15496  climle  15565  iserabs  15740  isumshft  15764  divcnvshft  15780  supcvg  15781  trireciplem  15787  expcnv  15789  explecnv  15790  geolim  15795  geo2lim  15800  cvgrat  15808  mertenslem2  15810  eftlub  16036  rpnnen2lem1  16141  rpnnen2lem2  16142  1arithlem1  16853  1arith  16857  vdwapval  16903  vdwlem6  16916  vdwlem9  16919  restfn  17346  cidffn  17602  idfu2nd  17802  idfu1st  17804  idfucl  17806  fucco  17890  homafval  17954  prf1  18124  prf2fval  18125  prfcl  18127  prf1st  18128  prf2nd  18129  curf1fval  18148  curf11  18150  curf12  18151  curf1cl  18152  curf2  18153  curfcl  18156  hof2val  18180  yonedalem3a  18198  yonedalem4a  18199  yonedalem4b  18200  yonedalem4c  18201  yonedalem3  18204  yonedainv  18205  lubfval  18272  glbfval  18285  smndex1gbas  18794  smndex1gid  18795  smndex1igid  18796  smndex1mnd  18802  smndex1id  18803  smndex1n0mnd  18804  smndex2dbas  18806  smndex2hbas  18808  cntzfval  19217  psgnfval  19397  sylow1lem2  19496  sylow2blem1  19517  sylow2blem2  19518  sylow3lem1  19524  sylow3lem6  19529  pj1fval  19591  vrgpfval  19663  rgspnval  20515  lspfval  20894  sraval  21097  irinitoringc  21404  zrhval2  21433  aspval  21798  psrmulfval  21868  psrass1  21889  mvrval  21907  mplmon  21958  mplcoe1  21960  evlslem2  22002  mpfrcl  22008  evlsval  22009  evlsvar  22013  mpfind  22030  mhpfval  22041  psdval  22062  psdmul  22069  coe1fval  22106  psropprmul  22138  coe1mul2  22171  ply1coe  22201  evls1fval  22222  evls1val  22223  evl1fval  22231  evl1val  22232  submafval  22482  mdetfval  22489  madufval  22540  minmar1fval  22549  pmatcollpw2lem  22680  pm2mpval  22698  1stcfb  23348  ptbasfi  23484  dfac14  23521  fmval  23846  fmf  23848  flffval  23892  fcfval  23936  cnextval  23964  met1stc  24425  pcoval  24927  iscmet3lem3  25206  rrxsca  25312  mbflimsup  25583  mbflim  25585  itg1climres  25631  mbfi1fseqlem2  25633  mbfi1fseqlem4  25635  mbfi1fseqlem6  25637  mbfi1flimlem  25639  mbfmullem2  25641  itg2monolem1  25667  itg2addlem  25675  itg2cnlem1  25678  cpnfval  25850  mdegfval  25983  elply  26116  plyeq0lem  26131  plypf1  26133  geolim3  26263  ulmuni  26317  ulmcau  26320  ulmdvlem1  26325  ulmdvlem3  26327  mbfulm  26331  itgulm  26333  pserval  26335  dvradcnv  26346  pserdvlem2  26354  abelthlem1  26357  abelthlem3  26359  abelthlem6  26362  logtayl  26585  leibpi  26868  dfef2  26897  emcllem4  26925  emcllem6  26927  emcllem7  26928  lgamgulmlem5  26959  lgamgulmlem6  26960  lgamcvg2  26981  basellem6  27012  sqff1o  27108  dchrptlem2  27192  dchrptlem3  27193  2lgslem1  27321  dchrisumlem3  27418  padicfval  27543  padicabvf  27558  istrkg2ld  28423  mirval  28618  ishpg  28722  lmif  28748  islmib  28750  axlowdim  28924  crctcshlem3  29782  nmoofval  30724  pjhfval  31358  pjmfn  31677  hosmval  31697  hommval  31698  hodmval  31699  hfsmval  31700  hfmmval  31701  eigvalfval  31859  brafval  31905  kbfval  31914  rnbra  32069  bra11  32070  padct  32676  fpwrelmap  32689  qusima  33355  nsgmgc  33359  nsgqusf1o  33363  idlsrgtset  33455  locfinreflem  33806  rspectopn  33833  zarcmplem  33847  ordtconnlem1  33890  xrhval  33984  sigapildsys  34128  sxbrsigalem2  34253  eulerpart  34349  dstfrvclim1  34445  ballotlemfval  34457  ballotlemsval  34476  signstfv  34530  vtsval  34604  cvmliftlem5  35261  mrsubffval  35479  mrsubfval  35480  msubffval  35495  msubfval  35496  msubrn  35501  msubco  35503  msubvrs  35532  circum  35646  divcnvlin  35705  climlec3  35706  faclimlem2  35716  faclim2  35720  knoppcnlem1  36466  knoppcnlem6  36471  knoppcnlem7  36472  cnndvlem2  36511  bj-endval  37288  ptrest  37598  poimirlem17  37616  poimirlem20  37619  voliunnfl  37643  volsupnfl  37644  upixp  37708  sdclem2  37721  fdc  37724  lmclim2  37737  geomcau  37738  rrncmslem  37811  pclfvalN  39868  polfvalN  39883  trlset  40140  tendopl  40755  docafvalN  41101  dibfval  41120  dibopelvalN  41122  dibopelval2  41124  dibelval3  41126  dibn0  41132  dib0  41143  diblsmopel  41150  dicn0  41171  dihopelvalcpre  41227  dihatlat  41313  dihpN  41315  dochfval  41329  lcfrlem9  41529  hvmapfval  41738  hvmapval  41739  hdmap1fval  41775  hlhilset  41913  sticksstones10  42128  sticksstones12a  42130  aks6d1c6isolem2  42148  evlsvvvallem2  42535  evlsvvval  42536  selvvvval  42558  evlselv  42560  prjcrvfval  42604  mzpincl  42707  dfac11  43035  dfac21  43039  hbtlem1  43096  hbtlem7  43098  fsovd  43981  mnringmulrcld  44201  dvgrat  44285  radcnvrat  44287  hashnzfzclim  44295  uzmptshftfval  44319  dvradcnv2  44320  binomcxplemrat  44323  binomcxplemcvg  44327  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  addrval  44439  subrval  44440  mulvval  44441  fmuldfeqlem1  45564  fmuldfeq  45565  clim1fr1  45583  climexp  45587  climneg  45592  climdivf  45594  divcnvg  45609  expfac  45639  climresmpt  45641  climsubmpt  45642  limsupval4  45776  climliminflimsupd  45783  liminfreuzlem  45784  liminfltlem  45786  liminfpnfuz  45798  dvsinax  45895  dvcosax  45908  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  dvnprodlem1  45928  dvnprodlem2  45929  dvnprodlem3  45930  stoweidlem59  46041  wallispilem5  46051  wallispi  46052  stirlinglem1  46056  stirlinglem8  46063  stirlinglem14  46069  stirlinglem15  46070  dirkerval  46073  fourierdlem71  46159  fourierdlem103  46191  fourierdlem104  46192  fourierdlem112  46200  etransclem48  46264  salgensscntex  46326  sge0tsms  46362  nnfoctbdjlem  46437  isomenndlem  46512  ovnval  46523  ovncvrrp  46546  ovnsubaddlem1  46552  hsphoif  46558  hsphoival  46561  ovnhoilem2  46584  hoidifhspval  46590  ovncvr2  46593  hspmbllem2  46609  vonioolem1  46662  smfpimcclem  46789  smflimsuplem1  46802  smflimsuplem4  46805  smflimsuplem7  46808  smfliminflem  46812  fsupdm  46824  smfsupdmmbllem  46826  finfdm  46828  smfinfdmmbllem  46830  cfsetsnfsetfo  47045  isuspgrim0  47879  cycldlenngric  47913  isgrtri  47928  1aryenef  48631  2aryenef  48642  itcovalpclem2  48657  itcovalt2lem2  48662  ackvalsuc1mpt  48664  ackval0  48666  cofidvala  49102  cofidval  49105  isnatd  49209  swapfelvv  49249  swapf2fvala  49250  swapf1vala  49252  swapf2fn  49254  swapf2vala  49256  tposcurf1  49285  prcofelvv  49366  reldmprcof1  49367  reldmprcof2  49368  prcof1  49374  prcof2a  49375  prcof2  49376  idfudiag1bas  49510  idfudiag1  49511  lmdfval  49635  cmdfval  49636  aacllem  49787