Theorem mptex 7209

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

Syntax hints:   ∈ wcel 2106  Vcvv 3473   ↦ cmpt 5224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540

This theorem is referenced by:  mptrabex  7211  mptfvmpt  7214  eufnfv  7215  fvresex  7928  ofmres  7953  noinfep  9637  cantnffval  9640  cnfcomlem  9676  cnfcom3clem  9682  ssttrcl  9692  ttrcltr  9693  ttrclselem2  9703  fseqenlem1  10001  dfacacn  10118  dfac12lem1  10120  infmap2  10195  ackbij2lem2  10217  ackbij2lem3  10218  fin23lem32  10321  konigthlem  10545  wunex2  10715  wuncval2  10724  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  mptnn0fsupp  13944  ccatfn  14504  ccatfval  14505  swrdval  14575  swrd00  14576  swrd0  14590  revval  14692  repsundef  14703  climmpt  15497  climle  15566  iserabs  15743  isumshft  15767  divcnvshft  15783  supcvg  15784  trireciplem  15790  expcnv  15792  explecnv  15793  geolim  15798  geo2lim  15803  cvgrat  15811  mertenslem2  15813  eftlub  16034  rpnnen2lem1  16139  rpnnen2lem2  16140  1arithlem1  16838  1arith  16842  vdwapval  16888  vdwlem6  16901  vdwlem9  16904  restfn  17352  cidffn  17604  idfu2nd  17809  idfu1st  17811  idfucl  17813  fucco  17897  homafval  17961  prf1  18134  prf2fval  18135  prfcl  18137  prf1st  18138  prf2nd  18139  curf1fval  18159  curf11  18161  curf12  18162  curf1cl  18163  curf2  18164  curfcl  18167  hof2val  18191  yonedalem3a  18209  yonedalem4a  18210  yonedalem4b  18211  yonedalem4c  18212  yonedalem3  18215  yonedainv  18216  lubfval  18285  glbfval  18298  smndex1gbas  18758  smndex1gid  18759  smndex1igid  18760  smndex1mnd  18766  smndex1id  18767  smndex1n0mnd  18768  smndex2dbas  18770  smndex2hbas  18772  cntzfval  19150  psgnfval  19332  sylow1lem2  19431  sylow2blem1  19452  sylow2blem2  19453  sylow3lem1  19459  sylow3lem6  19464  pj1fval  19526  vrgpfval  19598  lspfval  20533  sraval  20738  zrhval2  20991  aspval  21358  psrmulfval  21435  psrass1  21456  mvrval  21472  mplmon  21518  mplcoe1  21520  evlslem2  21571  mpfrcl  21577  evlsval  21578  evlsvar  21582  mpfind  21599  mhpfval  21611  coe1fval  21658  psropprmul  21691  coe1mul2  21722  ply1coe  21749  evls1fval  21767  evls1val  21768  evl1fval  21776  evl1val  21777  submafval  22010  mdetfval  22017  madufval  22068  minmar1fval  22077  pmatcollpw2lem  22208  pm2mpval  22226  1stcfb  22878  ptbasfi  23014  dfac14  23051  fmval  23376  fmf  23378  flffval  23422  fcfval  23466  cnextval  23494  met1stc  23959  pcoval  24456  iscmet3lem3  24736  rrxsca  24842  mbflimsup  25112  mbflim  25114  itg1climres  25161  mbfi1fseqlem2  25163  mbfi1fseqlem4  25165  mbfi1fseqlem6  25167  mbfi1flimlem  25169  mbfmullem2  25171  itg2monolem1  25197  itg2addlem  25205  itg2cnlem1  25208  cpnfval  25378  mdegfval  25509  elply  25638  plyeq0lem  25653  plypf1  25655  geolim3  25781  ulmuni  25833  ulmcau  25836  ulmdvlem1  25841  ulmdvlem3  25843  mbfulm  25847  itgulm  25849  pserval  25851  dvradcnv  25862  pserdvlem2  25869  abelthlem1  25872  abelthlem3  25874  abelthlem6  25877  logtayl  26097  leibpi  26374  dfef2  26402  emcllem4  26430  emcllem6  26432  emcllem7  26433  lgamgulmlem5  26464  lgamgulmlem6  26465  lgamcvg2  26486  basellem6  26517  sqff1o  26613  dchrptlem2  26695  dchrptlem3  26696  2lgslem1  26824  dchrisumlem3  26921  padicfval  27046  padicabvf  27061  istrkg2ld  27576  mirval  27771  ishpg  27875  lmif  27901  islmib  27903  axlowdim  28084  crctcshlem3  28938  nmoofval  29878  pjhfval  30512  pjmfn  30831  hosmval  30851  hommval  30852  hodmval  30853  hfsmval  30854  hfmmval  30855  eigvalfval  31013  brafval  31059  kbfval  31068  rnbra  31223  bra11  31224  padct  31815  fpwrelmap  31829  qusima  32376  nsgmgc  32379  nsgqusf1o  32383  idlsrgtset  32467  locfinreflem  32651  rspectopn  32678  zarcmplem  32692  ordtconnlem1  32735  xrhval  32829  sigapildsys  32991  sxbrsigalem2  33116  eulerpart  33212  dstfrvclim1  33307  ballotlemfval  33319  ballotlemsval  33338  signstfv  33405  vtsval  33480  cvmliftlem5  34111  mrsubffval  34329  mrsubfval  34330  msubffval  34345  msubfval  34346  msubrn  34351  msubco  34353  msubvrs  34382  circum  34490  divcnvlin  34532  climlec3  34533  faclimlem2  34544  faclim2  34548  knoppcnlem1  35173  knoppcnlem6  35178  knoppcnlem7  35179  cnndvlem2  35218  bj-endval  36000  ptrest  36291  poimirlem17  36309  poimirlem20  36312  voliunnfl  36336  volsupnfl  36337  upixp  36402  sdclem2  36415  fdc  36418  lmclim2  36431  geomcau  36432  rrncmslem  36505  pclfvalN  38565  polfvalN  38580  trlset  38837  tendopl  39452  docafvalN  39798  dibfval  39817  dibopelvalN  39819  dibopelval2  39821  dibelval3  39823  dibn0  39829  dib0  39840  diblsmopel  39847  dicn0  39868  dihopelvalcpre  39924  dihatlat  40010  dihpN  40012  dochfval  40026  lcfrlem9  40226  hvmapfval  40435  hvmapval  40436  hdmap1fval  40472  hlhilset  40610  sticksstones10  40776  sticksstones12a  40778  evlsbagval  40934  mhphf  40957  prjcrvfval  41155  mzpincl  41243  dfac11  41575  dfac21  41579  hbtlem1  41636  hbtlem7  41638  rgspnval  41681  fsovd  42530  mnringmulrcld  42758  dvgrat  42842  radcnvrat  42844  hashnzfzclim  42852  uzmptshftfval  42876  dvradcnv2  42877  binomcxplemrat  42880  binomcxplemcvg  42884  binomcxplemdvsum  42885  binomcxplemnotnn0  42886  addrval  42996  subrval  42997  mulvval  42998  fmuldfeqlem1  44071  fmuldfeq  44072  clim1fr1  44090  climexp  44094  climneg  44099  climdivf  44101  divcnvg  44116  expfac  44146  climresmpt  44148  climsubmpt  44149  limsupval4  44283  climliminflimsupd  44290  liminfreuzlem  44291  liminfltlem  44293  liminfpnfuz  44305  dvsinax  44402  dvcosax  44415  ioodvbdlimc1lem2  44421  ioodvbdlimc2lem  44423  dvnprodlem1  44435  dvnprodlem2  44436  dvnprodlem3  44437  stoweidlem59  44548  wallispilem5  44558  wallispi  44559  stirlinglem1  44563  stirlinglem8  44570  stirlinglem14  44576  stirlinglem15  44577  dirkerval  44580  fourierdlem71  44666  fourierdlem103  44698  fourierdlem104  44699  fourierdlem112  44707  etransclem48  44771  salgensscntex  44833  sge0tsms  44869  nnfoctbdjlem  44944  isomenndlem  45019  ovnval  45030  ovncvrrp  45053  ovnsubaddlem1  45059  hsphoif  45065  hsphoival  45068  ovnhoilem2  45091  hoidifhspval  45097  ovncvr2  45100  hspmbllem2  45116  vonioolem1  45169  smfpimcclem  45296  smflimsuplem1  45309  smflimsuplem4  45312  smflimsuplem7  45315  smfliminflem  45319  fsupdm  45331  smfsupdmmbllem  45333  finfdm  45335  smfinfdmmbllem  45337  cfsetsnfsetfo  45542  isomuspgrlem2  46273  irinitoringc  46615  1aryenef  46979  2aryenef  46990  itcovalpclem2  47005  itcovalt2lem2  47010  ackvalsuc1mpt  47012  ackval0  47014  aacllem  47496