Theorem mptex 7169

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440   ↦ cmpt 5179

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 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500

This theorem is referenced by:  mptrabex  7171  mptfvmpt  7174  eufnfv  7175  fvresex  7904  ofmres  7928  noinfep  9569  cantnffval  9572  cnfcomlem  9608  cnfcom3clem  9614  ssttrcl  9624  ttrcltr  9625  ttrclselem2  9635  fseqenlem1  9934  dfacacn  10052  dfac12lem1  10054  infmap2  10127  ackbij2lem2  10149  ackbij2lem3  10150  fin23lem32  10254  konigthlem  10479  wunex2  10649  wuncval2  10658  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  mptnn0fsupp  13920  ccatfn  14495  ccatfval  14496  swrdval  14567  swrd00  14568  swrd0  14582  revval  14683  repsundef  14694  climmpt  15494  climle  15563  iserabs  15738  isumshft  15762  divcnvshft  15778  supcvg  15779  trireciplem  15785  expcnv  15787  explecnv  15788  geolim  15793  geo2lim  15798  cvgrat  15806  mertenslem2  15808  eftlub  16034  rpnnen2lem1  16139  rpnnen2lem2  16140  1arithlem1  16851  1arith  16855  vdwapval  16901  vdwlem6  16914  vdwlem9  16917  restfn  17344  cidffn  17601  idfu2nd  17801  idfu1st  17803  idfucl  17805  fucco  17889  homafval  17953  prf1  18123  prf2fval  18124  prfcl  18126  prf1st  18127  prf2nd  18128  curf1fval  18147  curf11  18149  curf12  18150  curf1cl  18151  curf2  18152  curfcl  18155  hof2val  18179  yonedalem3a  18197  yonedalem4a  18198  yonedalem4b  18199  yonedalem4c  18200  yonedalem3  18203  yonedainv  18204  lubfval  18271  glbfval  18284  smndex1gbas  18827  smndex1gid  18828  smndex1igid  18829  smndex1mnd  18835  smndex1id  18836  smndex1n0mnd  18837  smndex2dbas  18839  smndex2hbas  18841  cntzfval  19249  psgnfval  19429  sylow1lem2  19528  sylow2blem1  19549  sylow2blem2  19550  sylow3lem1  19556  sylow3lem6  19561  pj1fval  19623  vrgpfval  19695  rgspnval  20545  lspfval  20924  sraval  21127  irinitoringc  21434  zrhval2  21463  aspval  21828  psrmulfval  21899  psrass1  21919  mvrval  21937  mplmon  21990  mplcoe1  21992  evlslem2  22034  mpfrcl  22040  evlsval  22041  evlsvvvallem2  22047  evlsvvval  22048  evlsvar  22050  mpfind  22070  mhpfval  22081  psdval  22102  psdmul  22109  coe1fval  22146  psropprmul  22178  coe1mul2  22211  ply1coe  22242  evls1fval  22263  evls1val  22264  evl1fval  22272  evl1val  22273  submafval  22523  mdetfval  22530  madufval  22581  minmar1fval  22590  pmatcollpw2lem  22721  pm2mpval  22739  1stcfb  23389  ptbasfi  23525  dfac14  23562  fmval  23887  fmf  23889  flffval  23933  fcfval  23977  cnextval  24005  met1stc  24465  pcoval  24967  iscmet3lem3  25246  rrxsca  25352  mbflimsup  25623  mbflim  25625  itg1climres  25671  mbfi1fseqlem2  25673  mbfi1fseqlem4  25675  mbfi1fseqlem6  25677  mbfi1flimlem  25679  mbfmullem2  25681  itg2monolem1  25707  itg2addlem  25715  itg2cnlem1  25718  cpnfval  25890  mdegfval  26023  elply  26156  plyeq0lem  26171  plypf1  26173  geolim3  26303  ulmuni  26357  ulmcau  26360  ulmdvlem1  26365  ulmdvlem3  26367  mbfulm  26371  itgulm  26373  pserval  26375  dvradcnv  26386  pserdvlem2  26394  abelthlem1  26397  abelthlem3  26399  abelthlem6  26402  logtayl  26625  leibpi  26908  dfef2  26937  emcllem4  26965  emcllem6  26967  emcllem7  26968  lgamgulmlem5  26999  lgamgulmlem6  27000  lgamcvg2  27021  basellem6  27052  sqff1o  27148  dchrptlem2  27232  dchrptlem3  27233  2lgslem1  27361  dchrisumlem3  27458  padicfval  27583  padicabvf  27598  istrkg2ld  28532  mirval  28727  ishpg  28831  lmif  28857  islmib  28859  axlowdim  29034  crctcshlem3  29892  nmoofval  30837  pjhfval  31471  pjmfn  31790  hosmval  31810  hommval  31811  hodmval  31812  hfsmval  31813  hfmmval  31814  eigvalfval  31972  brafval  32018  kbfval  32027  rnbra  32182  bra11  32183  padct  32797  fpwrelmap  32812  qusima  33489  nsgmgc  33493  nsgqusf1o  33497  idlsrgtset  33589  extvfval  33697  mplvrpmga  33710  esplyval  33720  locfinreflem  33997  rspectopn  34024  zarcmplem  34038  ordtconnlem1  34081  xrhval  34175  sigapildsys  34319  sxbrsigalem2  34443  eulerpart  34539  dstfrvclim1  34635  ballotlemfval  34647  ballotlemsval  34666  signstfv  34720  vtsval  34794  fineqvnttrclse  35280  cvmliftlem5  35483  mrsubffval  35701  mrsubfval  35702  msubffval  35717  msubfval  35718  msubrn  35723  msubco  35725  msubvrs  35754  circum  35868  divcnvlin  35927  climlec3  35928  faclimlem2  35938  faclim2  35942  knoppcnlem1  36693  knoppcnlem6  36698  knoppcnlem7  36699  cnndvlem2  36738  bj-endval  37516  ptrest  37816  poimirlem17  37834  poimirlem20  37837  voliunnfl  37861  volsupnfl  37862  upixp  37926  sdclem2  37939  fdc  37942  lmclim2  37955  geomcau  37956  rrncmslem  38029  pclfvalN  40145  polfvalN  40160  trlset  40417  tendopl  41032  docafvalN  41378  dibfval  41397  dibopelvalN  41399  dibopelval2  41401  dibelval3  41403  dibn0  41409  dib0  41420  diblsmopel  41427  dicn0  41448  dihopelvalcpre  41504  dihatlat  41590  dihpN  41592  dochfval  41606  lcfrlem9  41806  hvmapfval  42015  hvmapval  42016  hdmap1fval  42052  hlhilset  42190  sticksstones10  42405  sticksstones12a  42407  aks6d1c6isolem2  42425  selvvvval  42824  evlselv  42826  prjcrvfval  42870  mzpincl  42972  dfac11  43300  dfac21  43304  hbtlem1  43361  hbtlem7  43363  fsovd  44245  mnringmulrcld  44465  dvgrat  44549  radcnvrat  44551  hashnzfzclim  44559  uzmptshftfval  44583  dvradcnv2  44584  binomcxplemrat  44587  binomcxplemcvg  44591  binomcxplemdvsum  44592  binomcxplemnotnn0  44593  addrval  44702  subrval  44703  mulvval  44704  fmuldfeqlem1  45824  fmuldfeq  45825  clim1fr1  45843  climexp  45847  climneg  45852  climdivf  45854  divcnvg  45869  expfac  45897  climresmpt  45899  climsubmpt  45900  limsupval4  46034  climliminflimsupd  46041  liminfreuzlem  46042  liminfltlem  46044  liminfpnfuz  46056  dvsinax  46153  dvcosax  46166  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvnprodlem1  46186  dvnprodlem2  46187  dvnprodlem3  46188  stoweidlem59  46299  wallispilem5  46309  wallispi  46310  stirlinglem1  46314  stirlinglem8  46321  stirlinglem14  46327  stirlinglem15  46328  dirkerval  46331  fourierdlem71  46417  fourierdlem103  46449  fourierdlem104  46450  fourierdlem112  46458  etransclem48  46522  salgensscntex  46584  sge0tsms  46620  nnfoctbdjlem  46695  isomenndlem  46770  ovnval  46781  ovncvrrp  46804  ovnsubaddlem1  46810  hsphoif  46816  hsphoival  46819  ovnhoilem2  46842  hoidifhspval  46848  ovncvr2  46851  hspmbllem2  46867  vonioolem1  46920  smfpimcclem  47047  smflimsuplem1  47060  smflimsuplem4  47063  smflimsuplem7  47066  smfliminflem  47070  fsupdm  47082  smfsupdmmbllem  47084  finfdm  47086  smfinfdmmbllem  47088  cfsetsnfsetfo  47302  isuspgrim0  48136  cycldlenngric  48170  isgrtri  48185  1aryenef  48887  2aryenef  48898  itcovalpclem2  48913  itcovalt2lem2  48918  ackvalsuc1mpt  48920  ackval0  48922  cofidvala  49357  cofidval  49360  isnatd  49464  swapfelvv  49504  swapf2fvala  49505  swapf1vala  49507  swapf2fn  49509  swapf2vala  49511  tposcurf1  49540  prcofelvv  49621  reldmprcof1  49622  reldmprcof2  49623  prcof1  49629  prcof2a  49630  prcof2  49631  idfudiag1bas  49765  idfudiag1  49766  lmdfval  49890  cmdfval  49891  aacllem  50042