Theorem mptex 7166

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

Syntax hints:   ∈ wcel 2113  Vcvv 3438   ↦ cmpt 5176

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  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 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497

This theorem is referenced by:  mptrabex  7168  mptfvmpt  7171  eufnfv  7172  fvresex  7901  ofmres  7925  noinfep  9560  cantnffval  9563  cnfcomlem  9599  cnfcom3clem  9605  ssttrcl  9615  ttrcltr  9616  ttrclselem2  9626  fseqenlem1  9925  dfacacn  10043  dfac12lem1  10045  infmap2  10118  ackbij2lem2  10140  ackbij2lem3  10141  fin23lem32  10245  konigthlem  10469  wunex2  10639  wuncval2  10648  rpnnen1lem1  12886  rpnnen1lem3  12887  rpnnen1lem5  12889  mptnn0fsupp  13914  ccatfn  14489  ccatfval  14490  swrdval  14561  swrd00  14562  swrd0  14576  revval  14677  repsundef  14688  climmpt  15488  climle  15557  iserabs  15732  isumshft  15756  divcnvshft  15772  supcvg  15773  trireciplem  15779  expcnv  15781  explecnv  15782  geolim  15787  geo2lim  15792  cvgrat  15800  mertenslem2  15802  eftlub  16028  rpnnen2lem1  16133  rpnnen2lem2  16134  1arithlem1  16845  1arith  16849  vdwapval  16895  vdwlem6  16908  vdwlem9  16911  restfn  17338  cidffn  17594  idfu2nd  17794  idfu1st  17796  idfucl  17798  fucco  17882  homafval  17946  prf1  18116  prf2fval  18117  prfcl  18119  prf1st  18120  prf2nd  18121  curf1fval  18140  curf11  18142  curf12  18143  curf1cl  18144  curf2  18145  curfcl  18148  hof2val  18172  yonedalem3a  18190  yonedalem4a  18191  yonedalem4b  18192  yonedalem4c  18193  yonedalem3  18196  yonedainv  18197  lubfval  18264  glbfval  18277  smndex1gbas  18820  smndex1gid  18821  smndex1igid  18822  smndex1mnd  18828  smndex1id  18829  smndex1n0mnd  18830  smndex2dbas  18832  smndex2hbas  18834  cntzfval  19242  psgnfval  19422  sylow1lem2  19521  sylow2blem1  19542  sylow2blem2  19543  sylow3lem1  19549  sylow3lem6  19554  pj1fval  19616  vrgpfval  19688  rgspnval  20537  lspfval  20916  sraval  21119  irinitoringc  21426  zrhval2  21455  aspval  21820  psrmulfval  21890  psrass1  21911  mvrval  21929  mplmon  21980  mplcoe1  21982  evlslem2  22024  mpfrcl  22030  evlsval  22031  evlsvar  22035  mpfind  22052  mhpfval  22063  psdval  22084  psdmul  22091  coe1fval  22128  psropprmul  22160  coe1mul2  22193  ply1coe  22223  evls1fval  22244  evls1val  22245  evl1fval  22253  evl1val  22254  submafval  22504  mdetfval  22511  madufval  22562  minmar1fval  22571  pmatcollpw2lem  22702  pm2mpval  22720  1stcfb  23370  ptbasfi  23506  dfac14  23543  fmval  23868  fmf  23870  flffval  23914  fcfval  23958  cnextval  23986  met1stc  24446  pcoval  24948  iscmet3lem3  25227  rrxsca  25333  mbflimsup  25604  mbflim  25606  itg1climres  25652  mbfi1fseqlem2  25654  mbfi1fseqlem4  25656  mbfi1fseqlem6  25658  mbfi1flimlem  25660  mbfmullem2  25662  itg2monolem1  25688  itg2addlem  25696  itg2cnlem1  25699  cpnfval  25871  mdegfval  26004  elply  26137  plyeq0lem  26152  plypf1  26154  geolim3  26284  ulmuni  26338  ulmcau  26341  ulmdvlem1  26346  ulmdvlem3  26348  mbfulm  26352  itgulm  26354  pserval  26356  dvradcnv  26367  pserdvlem2  26375  abelthlem1  26378  abelthlem3  26380  abelthlem6  26383  logtayl  26606  leibpi  26889  dfef2  26918  emcllem4  26946  emcllem6  26948  emcllem7  26949  lgamgulmlem5  26980  lgamgulmlem6  26981  lgamcvg2  27002  basellem6  27033  sqff1o  27129  dchrptlem2  27213  dchrptlem3  27214  2lgslem1  27342  dchrisumlem3  27439  padicfval  27564  padicabvf  27579  istrkg2ld  28448  mirval  28643  ishpg  28747  lmif  28773  islmib  28775  axlowdim  28950  crctcshlem3  29808  nmoofval  30753  pjhfval  31387  pjmfn  31706  hosmval  31726  hommval  31727  hodmval  31728  hfsmval  31729  hfmmval  31730  eigvalfval  31888  brafval  31934  kbfval  31943  rnbra  32098  bra11  32099  padct  32712  fpwrelmap  32727  qusima  33384  nsgmgc  33388  nsgqusf1o  33392  idlsrgtset  33484  mplvrpmga  33586  esplyval  33596  locfinreflem  33864  rspectopn  33891  zarcmplem  33905  ordtconnlem1  33948  xrhval  34042  sigapildsys  34186  sxbrsigalem2  34310  eulerpart  34406  dstfrvclim1  34502  ballotlemfval  34514  ballotlemsval  34533  signstfv  34587  vtsval  34661  fineqvnttrclse  35155  cvmliftlem5  35344  mrsubffval  35562  mrsubfval  35563  msubffval  35578  msubfval  35579  msubrn  35584  msubco  35586  msubvrs  35615  circum  35729  divcnvlin  35788  climlec3  35789  faclimlem2  35799  faclim2  35803  knoppcnlem1  36548  knoppcnlem6  36553  knoppcnlem7  36554  cnndvlem2  36593  bj-endval  37370  ptrest  37669  poimirlem17  37687  poimirlem20  37690  voliunnfl  37714  volsupnfl  37715  upixp  37779  sdclem2  37792  fdc  37795  lmclim2  37808  geomcau  37809  rrncmslem  37882  pclfvalN  39998  polfvalN  40013  trlset  40270  tendopl  40885  docafvalN  41231  dibfval  41250  dibopelvalN  41252  dibopelval2  41254  dibelval3  41256  dibn0  41262  dib0  41273  diblsmopel  41280  dicn0  41301  dihopelvalcpre  41357  dihatlat  41443  dihpN  41445  dochfval  41459  lcfrlem9  41659  hvmapfval  41868  hvmapval  41869  hdmap1fval  41905  hlhilset  42043  sticksstones10  42258  sticksstones12a  42260  aks6d1c6isolem2  42278  evlsvvvallem2  42670  evlsvvval  42671  selvvvval  42693  evlselv  42695  prjcrvfval  42739  mzpincl  42841  dfac11  43169  dfac21  43173  hbtlem1  43230  hbtlem7  43232  fsovd  44115  mnringmulrcld  44335  dvgrat  44419  radcnvrat  44421  hashnzfzclim  44429  uzmptshftfval  44453  dvradcnv2  44454  binomcxplemrat  44457  binomcxplemcvg  44461  binomcxplemdvsum  44462  binomcxplemnotnn0  44463  addrval  44572  subrval  44573  mulvval  44574  fmuldfeqlem1  45696  fmuldfeq  45697  clim1fr1  45715  climexp  45719  climneg  45724  climdivf  45726  divcnvg  45741  expfac  45769  climresmpt  45771  climsubmpt  45772  limsupval4  45906  climliminflimsupd  45913  liminfreuzlem  45914  liminfltlem  45916  liminfpnfuz  45928  dvsinax  46025  dvcosax  46038  ioodvbdlimc1lem2  46044  ioodvbdlimc2lem  46046  dvnprodlem1  46058  dvnprodlem2  46059  dvnprodlem3  46060  stoweidlem59  46171  wallispilem5  46181  wallispi  46182  stirlinglem1  46186  stirlinglem8  46193  stirlinglem14  46199  stirlinglem15  46200  dirkerval  46203  fourierdlem71  46289  fourierdlem103  46321  fourierdlem104  46322  fourierdlem112  46330  etransclem48  46394  salgensscntex  46456  sge0tsms  46492  nnfoctbdjlem  46567  isomenndlem  46642  ovnval  46653  ovncvrrp  46676  ovnsubaddlem1  46682  hsphoif  46688  hsphoival  46691  ovnhoilem2  46714  hoidifhspval  46720  ovncvr2  46723  hspmbllem2  46739  vonioolem1  46792  smfpimcclem  46919  smflimsuplem1  46932  smflimsuplem4  46935  smflimsuplem7  46938  smfliminflem  46942  fsupdm  46954  smfsupdmmbllem  46956  finfdm  46958  smfinfdmmbllem  46960  cfsetsnfsetfo  47174  isuspgrim0  48008  cycldlenngric  48042  isgrtri  48057  1aryenef  48760  2aryenef  48771  itcovalpclem2  48786  itcovalt2lem2  48791  ackvalsuc1mpt  48793  ackval0  48795  cofidvala  49231  cofidval  49234  isnatd  49338  swapfelvv  49378  swapf2fvala  49379  swapf1vala  49381  swapf2fn  49383  swapf2vala  49385  tposcurf1  49414  prcofelvv  49495  reldmprcof1  49496  reldmprcof2  49497  prcof1  49503  prcof2a  49504  prcof2  49505  idfudiag1bas  49639  idfudiag1  49640  lmdfval  49764  cmdfval  49765  aacllem  49916