Theorem mptex 7211

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

Syntax hints:   ∈ wcel 2145  Vcvv 3457   ↦ cmpt 5186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533

This theorem is referenced by:  mptrabex  7213  mptfvmpt  7216  eufnfv  7217  fvresex  7945  ofmres  7969  noinfep  9617  cantnffval  9620  cnfcomlem  9656  cnfcom3clem  9662  ssttrcl  9672  ttrcltr  9673  ttrclselem2  9683  fseqenlem1  9996  dfacacn  10113  dfac12lem1  10115  infmap2  10188  ackbij2lem2  10210  ackbij2lem3  10211  fin23lem32  10316  konigthlem  10541  wunex2  10711  wuncval2  10720  rpnnen1lem1  12993  rpnnen1lem3  12994  rpnnen1lem5  12996  mptnn0fsupp  14024  ccatfn  14599  ccatfval  14600  swrdval  14671  swrd00  14672  swrd0  14686  revval  14787  repsundef  14798  climmpt  15612  climle  15681  iserabs  15857  isumshft  15883  divcnvshft  15899  supcvg  15900  trireciplem  15906  expcnv  15908  explecnv  15909  geolim  15914  geo2lim  15919  cvgrat  15927  mertenslem2  15929  eftlub  16155  rpnnen2lem1  16260  rpnnen2lem2  16261  1arithlem1  16973  1arith  16977  vdwapval  17023  vdwlem6  17036  vdwlem9  17039  restfn  17467  cidffn  17724  idfu2nd  17924  idfu1st  17926  idfucl  17928  fucco  18012  homafval  18076  prf1  18246  prf2fval  18247  prfcl  18249  prf1st  18250  prf2nd  18251  curf1fval  18270  curf11  18272  curf12  18273  curf1cl  18274  curf2  18275  curfcl  18278  hof2val  18302  yonedalem3a  18320  yonedalem4a  18321  yonedalem4b  18322  yonedalem4c  18323  yonedalem3  18326  yonedainv  18327  lubfval  18394  glbfval  18407  smndex1gbasOLD  18952  smndex1gidOLD  18954  smndex1igidOLD  18956  smndex1mnd  18962  smndex1id  18963  smndex1n0mnd  18964  smndex2dbas  18966  smndex2hbas  18968  cntzfval  19381  psgnfval  19561  sylow1lem2  19660  sylow2blem1  19681  sylow2blem2  19682  sylow3lem1  19688  sylow3lem6  19693  pj1fval  19755  vrgpfval  19827  rgspnval  20688  lspfval  21063  sraval  21265  irinitoringc  21589  zrhval2  21618  aspval  21982  psrmulfval  22053  psrass1  22073  mvrval  22091  mplmon  22146  mplcoe1  22148  evlslem2  22190  mpfrcl  22196  evlsval  22197  evlsvvvallem2  22203  evlsvvval  22204  evlsvar  22206  mpfind  22226  selvvvval  22253  mhpfval  22261  psdval  22282  psdmul  22289  coe1fval  22325  psropprmul  22357  coe1mul2  22390  ply1coe  22419  evls1fval  22440  evls1val  22441  evl1fval  22449  evl1val  22450  submafval  22697  mdetfval  22704  madufval  22755  minmar1fval  22764  pmatcollpw2lem  22895  pm2mpval  22913  1stcfb  23563  ptbasfi  23699  dfac14  23736  fmval  24061  fmf  24063  flffval  24107  fcfval  24151  cnextval  24179  met1stc  24639  pcoval  25131  iscmet3lem3  25410  rrxsca  25516  mbflimsup  25786  mbflim  25788  itg1climres  25834  mbfi1fseqlem2  25836  mbfi1fseqlem4  25838  mbfi1fseqlem6  25840  mbfi1flimlem  25842  mbfmullem2  25844  itg2monolem1  25870  itg2addlem  25878  itg2cnlem1  25881  cpnfval  26052  mdegfval  26180  elply  26313  plyeq0lem  26328  plypf1  26330  geolim3  26461  ulmuni  26513  ulmcau  26516  ulmdvlem1  26521  ulmdvlem3  26523  mbfulm  26527  itgulm  26529  pserval  26531  dvradcnv  26542  pserdvlem2  26549  abelthlem1  26552  abelthlem3  26554  abelthlem6  26557  logtayl  26783  leibpi  27065  dfef2  27093  emcllem4  27121  emcllem6  27123  emcllem7  27124  lgamgulmlem5  27155  lgamgulmlem6  27156  lgamcvg2  27177  basellem6  27208  sqff1o  27304  dchrptlem2  27387  dchrptlem3  27388  2lgslem1  27516  dchrisumlem3  27613  padicfval  27738  padicabvf  27753  mirval  28886  ishpg  28990  lmif  29037  islmib  29039  axlowdim  29220  crctcshlem3  30077  nmoofval  31023  pjhfval  31657  pjmfn  31976  hosmval  31996  hommval  31997  hodmval  31998  hfsmval  31999  hfmmval  32000  eigvalfval  32158  brafval  32204  kbfval  32213  rnbra  32368  bra11  32369  fpwrelmap  32990  qusima  33633  nsgmgc  33637  nsgqusf1o  33641  idlsrgtset  33715  extvfval  33839  mplvrpmga  33852  esplyval  33869  locfinreflem  34147  rspectopn  34174  zarcmplem  34188  ordtconnlem1  34231  xrhval  34325  sigapildsys  34469  sxbrsigalem2  34593  eulerpart  34689  dstfrvclim1  34785  ballotlemfval  34797  ballotlemsval  34816  signstfv  34867  vtsval  34941  fineqvnttrclse  35432  cvmliftlem5  35652  mrsubffval  35870  mrsubfval  35871  msubffval  35886  msubfval  35887  msubrn  35892  msubco  35894  msubvrs  35923  circum  36037  divcnvlin  36096  climlec3  36097  faclimlem2  36107  faclim2  36111  knoppcnlem1  36944  knoppcnlem6  36949  knoppcnlem7  36950  cnndvlem2  36989  bj-endval  37819  ptrest  38130  poimirlem17  38148  poimirlem20  38151  voliunnfl  38175  volsupnfl  38176  upixp  38240  sdclem2  38253  fdc  38256  lmclim2  38269  geomcau  38270  rrncmslem  38343  pclfvalN  40525  polfvalN  40540  trlset  40797  tendopl  41412  docafvalN  41758  dibfval  41777  dibopelvalN  41779  dibopelval2  41781  dibelval3  41783  dibn0  41789  dib0  41800  diblsmopel  41807  dicn0  41828  dihopelvalcpre  41884  dihatlat  41970  dihpN  41972  dochfval  41986  lcfrlem9  42186  hvmapfval  42395  hvmapval  42396  hdmap1fval  42432  hlhilset  42570  sticksstones10  42784  sticksstones12a  42786  aks6d1c6isolem2  42804  evlselv  43183  prjcrvfval  43225  mzpincl  43327  dfac11  43651  dfac21  43655  hbtlem1  43712  hbtlem7  43714  fsovd  44596  mnringmulrcld  44816  dvgrat  44886  radcnvrat  44888  hashnzfzclim  44896  uzmptshftfval  44920  dvradcnv2  44921  binomcxplemrat  44924  binomcxplemcvg  44928  binomcxplemdvsum  44929  binomcxplemnotnn0  44930  addrval  45039  subrval  45040  mulvval  45041  fmuldfeqlem1  46156  fmuldfeq  46157  clim1fr1  46175  climexp  46179  climneg  46184  climdivf  46186  divcnvg  46201  expfac  46229  climresmpt  46231  climsubmpt  46232  limsupval4  46366  climliminflimsupd  46373  liminfreuzlem  46374  liminfltlem  46376  liminfpnfuz  46388  dvsinax  46485  dvcosax  46498  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  dvnprodlem1  46518  dvnprodlem2  46519  dvnprodlem3  46520  stoweidlem59  46631  wallispilem5  46641  wallispi  46642  stirlinglem1  46646  stirlinglem8  46653  stirlinglem14  46659  stirlinglem15  46660  dirkerval  46663  fourierdlem71  46749  fourierdlem103  46781  fourierdlem104  46782  fourierdlem112  46790  etransclem48  46854  salgensscntex  46916  sge0tsms  46952  nnfoctbdjlem  47027  isomenndlem  47102  ovnval  47113  ovncvrrp  47136  ovnsubaddlem1  47142  hsphoif  47148  hsphoival  47151  ovnhoilem2  47174  hoidifhspval  47180  ovncvr2  47183  hspmbllem2  47199  vonioolem1  47252  smfpimcclem  47379  smflimsuplem1  47392  smflimsuplem4  47395  smflimsuplem7  47398  smfliminflem  47402  fsupdm  47414  smfsupdmmbllem  47416  finfdm  47418  smfinfdmmbllem  47420  cfsetsnfsetfo  47652  isuspgrim0  48514  cycldlenngric  48548  isgrtri  48563  1aryenef  49276  2aryenef  49287  itcovalpclem2  49302  itcovalt2lem2  49307  ackvalsuc1mpt  49309  ackval0  49311  cofidvala  49745  cofidval  49748  isnatd  49852  swapfelvv  49892  swapf2fvala  49893  swapf1vala  49895  swapf2fn  49897  swapf2vala  49899  tposcurf1  49928  prcofelvv  50009  reldmprcof1  50010  reldmprcof2  50011  prcof1  50017  prcof2a  50018  prcof2  50019  idfudiag1bas  50153  idfudiag1  50154  lmdfval  50278  cmdfval  50279  aacllem  50430