Theorem mptex 6986

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

Syntax hints:   ∈ wcel 2114  Vcvv 3494   ↦ cmpt 5146

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 5190  ax-sep 5203  ax-nul 5210  ax-pr 5330

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 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363

This theorem is referenced by:  mptrabex  6988  mptfvmpt  6990  eufnfv  6991  fvresex  7661  ofmres  7685  noinfep  9123  cantnffval  9126  cnfcomlem  9162  cnfcom3clem  9168  fseqenlem1  9450  dfacacn  9567  dfac12lem1  9569  infmap2  9640  ackbij2lem2  9662  ackbij2lem3  9663  fin23lem32  9766  konigthlem  9990  wunex2  10160  wuncval2  10169  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem5  12381  mptnn0fsupp  13366  ccatfn  13924  ccatfval  13925  swrdval  14005  swrd00  14006  swrd0  14020  revval  14122  repsundef  14133  climmpt  14928  climle  14996  iserabs  15170  isumshft  15194  divcnvshft  15210  supcvg  15211  trireciplem  15217  expcnv  15219  explecnv  15220  geolim  15226  geo2lim  15231  cvgrat  15239  mertenslem2  15241  eftlub  15462  rpnnen2lem1  15567  rpnnen2lem2  15568  1arithlem1  16259  1arith  16263  vdwapval  16309  vdwlem6  16322  vdwlem9  16325  restfn  16698  cidffn  16949  idfu2nd  17147  idfu1st  17149  idfucl  17151  fucco  17232  homafval  17289  prf1  17450  prf2fval  17451  prfcl  17453  prf1st  17454  prf2nd  17455  curf1fval  17474  curf11  17476  curf12  17477  curf1cl  17478  curf2  17479  curfcl  17482  hof2val  17506  yonedalem3a  17524  yonedalem4a  17525  yonedalem4b  17526  yonedalem4c  17527  yonedalem3  17530  yonedainv  17531  lubfval  17588  glbfval  17601  smndex1gbas  18067  smndex1gid  18068  smndex1igid  18069  smndex1mnd  18075  smndex1id  18076  smndex1n0mnd  18077  smndex2dbas  18079  smndex2hbas  18081  cntzfval  18450  psgnfval  18628  sylow1lem2  18724  sylow2blem1  18745  sylow2blem2  18746  sylow3lem1  18752  sylow3lem6  18757  pj1fval  18820  vrgpfval  18892  lspfval  19745  sraval  19948  aspval  20102  psrmulfval  20165  psrass1  20185  mvrval  20201  mplmon  20244  mplcoe1  20246  evlslem2  20292  mpfrcl  20298  evlsval  20299  evlsvar  20303  mpfind  20320  mhpfval  20332  coe1fval  20373  psropprmul  20406  coe1mul2  20437  ply1coe  20464  evls1fval  20482  evls1val  20483  evl1fval  20491  evl1val  20492  zrhval2  20656  submafval  21188  mdetfval  21195  madufval  21246  minmar1fval  21255  pmatcollpw2lem  21385  pm2mpval  21403  1stcfb  22053  ptbasfi  22189  dfac14  22226  fmval  22551  fmf  22553  flffval  22597  fcfval  22641  cnextval  22669  met1stc  23131  pcoval  23615  iscmet3lem3  23893  rrxsca  23999  mbflimsup  24267  mbflim  24269  itg1climres  24315  mbfi1fseqlem2  24317  mbfi1fseqlem4  24319  mbfi1fseqlem6  24321  mbfi1flimlem  24323  mbfmullem2  24325  itg2monolem1  24351  itg2addlem  24359  itg2cnlem1  24362  cpnfval  24529  mdegfval  24656  elply  24785  plyeq0lem  24800  plypf1  24802  geolim3  24928  ulmuni  24980  ulmcau  24983  ulmdvlem1  24988  ulmdvlem3  24990  mbfulm  24994  itgulm  24996  pserval  24998  dvradcnv  25009  pserdvlem2  25016  abelthlem1  25019  abelthlem3  25021  abelthlem6  25024  logtayl  25243  leibpi  25520  dfef2  25548  emcllem4  25576  emcllem6  25578  emcllem7  25579  lgamgulmlem5  25610  lgamgulmlem6  25611  lgamcvg2  25632  basellem6  25663  sqff1o  25759  dchrptlem2  25841  dchrptlem3  25842  2lgslem1  25970  dchrisumlem3  26067  padicfval  26192  padicabvf  26207  istrkg2ld  26246  mirval  26441  ishpg  26545  lmif  26571  islmib  26573  axlowdim  26747  crctcshlem3  27597  nmoofval  28539  pjhfval  29173  pjmfn  29492  hosmval  29512  hommval  29513  hodmval  29514  hfsmval  29515  hfmmval  29516  eigvalfval  29674  brafval  29720  kbfval  29729  rnbra  29884  bra11  29885  padct  30455  fpwrelmap  30469  locfinreflem  31104  ordtconnlem1  31167  xrhval  31259  sigapildsys  31421  sxbrsigalem2  31544  eulerpart  31640  dstfrvclim1  31735  ballotlemfval  31747  ballotlemsval  31766  signstfv  31833  vtsval  31908  cvmliftlem5  32536  mrsubffval  32754  mrsubfval  32755  msubffval  32770  msubfval  32771  msubrn  32776  msubco  32778  msubvrs  32807  circum  32917  divcnvlin  32964  climlec3  32965  faclimlem2  32976  faclim2  32980  knoppcnlem1  33832  knoppcnlem6  33837  knoppcnlem7  33838  cnndvlem2  33877  bj-endval  34599  ptrest  34906  poimirlem17  34924  poimirlem20  34927  voliunnfl  34951  volsupnfl  34952  upixp  35019  sdclem2  35032  fdc  35035  lmclim2  35048  geomcau  35049  rrncmslem  35125  pclfvalN  37040  polfvalN  37055  trlset  37312  tendopl  37927  docafvalN  38273  dibfval  38292  dibopelvalN  38294  dibopelval2  38296  dibelval3  38298  dibn0  38304  dib0  38315  diblsmopel  38322  dicn0  38343  dihopelvalcpre  38399  dihatlat  38485  dihpN  38487  dochfval  38501  lcfrlem9  38701  hvmapfval  38910  hvmapval  38911  hdmap1fval  38947  hlhilset  39085  mzpincl  39351  dfac11  39682  dfac21  39686  hbtlem1  39743  hbtlem7  39745  rgspnval  39788  fsovd  40374  dvgrat  40664  radcnvrat  40666  hashnzfzclim  40674  uzmptshftfval  40698  dvradcnv2  40699  binomcxplemrat  40702  binomcxplemcvg  40706  binomcxplemdvsum  40707  binomcxplemnotnn0  40708  addrval  40818  subrval  40819  mulvval  40820  fmuldfeqlem1  41883  fmuldfeq  41884  clim1fr1  41902  climexp  41906  climneg  41911  climdivf  41913  divcnvg  41928  expfac  41958  climresmpt  41960  climsubmpt  41961  limsupval4  42095  climliminflimsupd  42102  liminfreuzlem  42103  liminfltlem  42105  liminfpnfuz  42117  dvsinax  42217  dvcosax  42231  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvnprodlem1  42251  dvnprodlem2  42252  dvnprodlem3  42253  stoweidlem59  42364  wallispilem5  42374  wallispi  42375  stirlinglem1  42379  stirlinglem8  42386  stirlinglem14  42392  stirlinglem15  42393  dirkerval  42396  fourierdlem71  42482  fourierdlem103  42514  fourierdlem104  42515  fourierdlem112  42523  etransclem48  42587  salgensscntex  42647  sge0tsms  42682  nnfoctbdjlem  42757  isomenndlem  42832  ovnval  42843  ovncvrrp  42866  ovnsubaddlem1  42872  hsphoif  42878  hsphoival  42881  ovnhoilem2  42904  hoidifhspval  42910  ovncvr2  42913  hspmbllem2  42929  vonioolem1  42982  smfpimcclem  43101  smflimsuplem1  43114  smflimsuplem4  43117  smflimsuplem7  43120  smfliminflem  43124  isomuspgrlem2  44018  irinitoringc  44360  aacllem  44922