Theorem mptex 6972

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

Syntax hints:   ∈ wcel 2114  Vcvv 3486   ↦ cmpt 5132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pr 5316

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349

This theorem is referenced by:  mptrabex  6974  mptfvmpt  6976  eufnfv  6977  fvresex  7647  ofmres  7671  noinfep  9109  cantnffval  9112  cnfcomlem  9148  cnfcom3clem  9154  fseqenlem1  9436  dfacacn  9553  dfac12lem1  9555  infmap2  9626  ackbij2lem2  9648  ackbij2lem3  9649  fin23lem32  9752  konigthlem  9976  wunex2  10146  wuncval2  10155  rpnnen1lem1  12364  rpnnen1lem3  12365  rpnnen1lem5  12367  mptnn0fsupp  13355  ccatfn  13909  ccatfval  13910  swrdval  13990  swrd00  13991  swrd0  14005  revval  14107  repsundef  14118  climmpt  14913  climle  14981  iserabs  15155  isumshft  15179  divcnvshft  15195  supcvg  15196  trireciplem  15202  expcnv  15204  explecnv  15205  geolim  15211  geo2lim  15216  cvgrat  15224  mertenslem2  15226  eftlub  15447  rpnnen2lem1  15552  rpnnen2lem2  15553  1arithlem1  16242  1arith  16246  vdwapval  16292  vdwlem6  16305  vdwlem9  16308  restfn  16681  cidffn  16932  idfu2nd  17130  idfu1st  17132  idfucl  17134  fucco  17215  homafval  17272  prf1  17433  prf2fval  17434  prfcl  17436  prf1st  17437  prf2nd  17438  curf1fval  17457  curf11  17459  curf12  17460  curf1cl  17461  curf2  17462  curfcl  17465  hof2val  17489  yonedalem3a  17507  yonedalem4a  17508  yonedalem4b  17509  yonedalem4c  17510  yonedalem3  17513  yonedainv  17514  lubfval  17571  glbfval  17584  smndex1gbas  18050  smndex1gid  18051  smndex1igid  18052  smndex1mnd  18058  smndex1id  18059  smndex1n0mnd  18060  smndex2dbas  18062  smndex2hbas  18064  cntzfval  18433  psgnfval  18611  sylow1lem2  18707  sylow2blem1  18728  sylow2blem2  18729  sylow3lem1  18735  sylow3lem6  18740  pj1fval  18803  vrgpfval  18875  lspfval  19728  sraval  19931  aspval  20085  psrmulfval  20148  psrass1  20168  mvrval  20184  mplmon  20227  mplcoe1  20229  evlslem2  20275  mpfrcl  20281  evlsval  20282  evlsvar  20286  mpfind  20303  mhpfval  20315  coe1fval  20356  psropprmul  20389  coe1mul2  20420  ply1coe  20447  evls1fval  20465  evls1val  20466  evl1fval  20474  evl1val  20475  zrhval2  20639  submafval  21171  mdetfval  21178  madufval  21229  minmar1fval  21238  pmatcollpw2lem  21368  pm2mpval  21386  1stcfb  22036  ptbasfi  22172  dfac14  22209  fmval  22534  fmf  22536  flffval  22580  fcfval  22624  cnextval  22652  met1stc  23114  pcoval  23598  iscmet3lem3  23876  rrxsca  23982  mbflimsup  24250  mbflim  24252  itg1climres  24298  mbfi1fseqlem2  24300  mbfi1fseqlem4  24302  mbfi1fseqlem6  24304  mbfi1flimlem  24306  mbfmullem2  24308  itg2monolem1  24334  itg2addlem  24342  itg2cnlem1  24345  cpnfval  24514  mdegfval  24642  elply  24771  plyeq0lem  24786  plypf1  24788  geolim3  24914  ulmuni  24966  ulmcau  24969  ulmdvlem1  24974  ulmdvlem3  24976  mbfulm  24980  itgulm  24982  pserval  24984  dvradcnv  24995  pserdvlem2  25002  abelthlem1  25005  abelthlem3  25007  abelthlem6  25010  logtayl  25229  leibpi  25506  dfef2  25534  emcllem4  25562  emcllem6  25564  emcllem7  25565  lgamgulmlem5  25596  lgamgulmlem6  25597  lgamcvg2  25618  basellem6  25649  sqff1o  25745  dchrptlem2  25827  dchrptlem3  25828  2lgslem1  25956  dchrisumlem3  26053  padicfval  26178  padicabvf  26193  istrkg2ld  26232  mirval  26427  ishpg  26531  lmif  26557  islmib  26559  axlowdim  26733  crctcshlem3  27583  nmoofval  28523  pjhfval  29157  pjmfn  29476  hosmval  29496  hommval  29497  hodmval  29498  hfsmval  29499  hfmmval  29500  eigvalfval  29658  brafval  29704  kbfval  29713  rnbra  29868  bra11  29869  padct  30441  fpwrelmap  30455  locfinreflem  31114  ordtconnlem1  31174  xrhval  31266  sigapildsys  31428  sxbrsigalem2  31551  eulerpart  31647  dstfrvclim1  31742  ballotlemfval  31754  ballotlemsval  31773  signstfv  31840  vtsval  31915  cvmliftlem5  32543  mrsubffval  32761  mrsubfval  32762  msubffval  32777  msubfval  32778  msubrn  32783  msubco  32785  msubvrs  32814  circum  32924  divcnvlin  32971  climlec3  32972  faclimlem2  32983  faclim2  32987  knoppcnlem1  33839  knoppcnlem6  33844  knoppcnlem7  33845  cnndvlem2  33884  bj-endval  34612  ptrest  34925  poimirlem17  34943  poimirlem20  34946  voliunnfl  34970  volsupnfl  34971  upixp  35036  sdclem2  35049  fdc  35052  lmclim2  35065  geomcau  35066  rrncmslem  35142  pclfvalN  37057  polfvalN  37072  trlset  37329  tendopl  37944  docafvalN  38290  dibfval  38309  dibopelvalN  38311  dibopelval2  38313  dibelval3  38315  dibn0  38321  dib0  38332  diblsmopel  38339  dicn0  38360  dihopelvalcpre  38416  dihatlat  38502  dihpN  38504  dochfval  38518  lcfrlem9  38718  hvmapfval  38927  hvmapval  38928  hdmap1fval  38964  hlhilset  39102  mzpincl  39423  dfac11  39754  dfac21  39758  hbtlem1  39815  hbtlem7  39817  rgspnval  39860  fsovd  40444  dvgrat  40734  radcnvrat  40736  hashnzfzclim  40744  uzmptshftfval  40768  dvradcnv2  40769  binomcxplemrat  40772  binomcxplemcvg  40776  binomcxplemdvsum  40777  binomcxplemnotnn0  40778  addrval  40888  subrval  40889  mulvval  40890  fmuldfeqlem1  41953  fmuldfeq  41954  clim1fr1  41972  climexp  41976  climneg  41981  climdivf  41983  divcnvg  41998  expfac  42028  climresmpt  42030  climsubmpt  42031  limsupval4  42165  climliminflimsupd  42172  liminfreuzlem  42173  liminfltlem  42175  liminfpnfuz  42187  dvsinax  42287  dvcosax  42301  ioodvbdlimc1lem2  42307  ioodvbdlimc2lem  42309  dvnprodlem1  42321  dvnprodlem2  42322  dvnprodlem3  42323  stoweidlem59  42434  wallispilem5  42444  wallispi  42445  stirlinglem1  42449  stirlinglem8  42456  stirlinglem14  42462  stirlinglem15  42463  dirkerval  42466  fourierdlem71  42552  fourierdlem103  42584  fourierdlem104  42585  fourierdlem112  42593  etransclem48  42657  salgensscntex  42717  sge0tsms  42752  nnfoctbdjlem  42827  isomenndlem  42902  ovnval  42913  ovncvrrp  42936  ovnsubaddlem1  42942  hsphoif  42948  hsphoival  42951  ovnhoilem2  42974  hoidifhspval  42980  ovncvr2  42983  hspmbllem2  42999  vonioolem1  43052  smfpimcclem  43171  smflimsuplem1  43184  smflimsuplem4  43187  smflimsuplem7  43190  smfliminflem  43194  isomuspgrlem2  44083  irinitoringc  44425  aacllem  44987