Theorem mptex 7203

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453   ↦ cmpt 5180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525

This theorem is referenced by:  mptrabex  7205  mptfvmpt  7208  eufnfv  7209  fvresex  7937  ofmres  7961  noinfep  9612  cantnffval  9615  cnfcomlem  9651  cnfcom3clem  9657  ssttrcl  9667  ttrcltr  9668  ttrclselem2  9678  fseqenlem1  9977  dfacacn  10095  dfac12lem1  10097  infmap2  10170  ackbij2lem2  10192  ackbij2lem3  10193  fin23lem32  10298  konigthlem  10523  wunex2  10693  wuncval2  10702  rpnnen1lem1  12976  rpnnen1lem3  12977  rpnnen1lem5  12979  mptnn0fsupp  14007  ccatfn  14582  ccatfval  14583  swrdval  14654  swrd00  14655  swrd0  14669  revval  14770  repsundef  14781  climmpt  15581  climle  15650  iserabs  15826  isumshft  15852  divcnvshft  15868  supcvg  15869  trireciplem  15875  expcnv  15877  explecnv  15878  geolim  15883  geo2lim  15888  cvgrat  15896  mertenslem2  15898  eftlub  16124  rpnnen2lem1  16229  rpnnen2lem2  16230  1arithlem1  16942  1arith  16946  vdwapval  16992  vdwlem6  17005  vdwlem9  17008  restfn  17436  cidffn  17693  idfu2nd  17893  idfu1st  17895  idfucl  17897  fucco  17981  homafval  18045  prf1  18215  prf2fval  18216  prfcl  18218  prf1st  18219  prf2nd  18220  curf1fval  18239  curf11  18241  curf12  18242  curf1cl  18243  curf2  18244  curfcl  18247  hof2val  18271  yonedalem3a  18289  yonedalem4a  18290  yonedalem4b  18291  yonedalem4c  18292  yonedalem3  18295  yonedainv  18296  lubfval  18363  glbfval  18376  smndex1gbasOLD  18920  smndex1gidOLD  18922  smndex1igidOLD  18924  smndex1mnd  18930  smndex1id  18931  smndex1n0mnd  18932  smndex2dbas  18934  smndex2hbas  18936  cntzfval  19343  psgnfval  19523  sylow1lem2  19622  sylow2blem1  19643  sylow2blem2  19644  sylow3lem1  19650  sylow3lem6  19655  pj1fval  19717  vrgpfval  19789  rgspnval  20641  lspfval  21020  sraval  21222  irinitoringc  21511  zrhval2  21540  aspval  21904  psrmulfval  21975  psrass1  21995  mvrval  22013  mplmon  22068  mplcoe1  22070  evlslem2  22112  mpfrcl  22118  evlsval  22119  evlsvvvallem2  22125  evlsvvval  22126  evlsvar  22128  mpfind  22148  selvvvval  22175  mhpfval  22183  psdval  22204  psdmul  22211  coe1fval  22247  psropprmul  22279  coe1mul2  22312  ply1coe  22341  evls1fval  22362  evls1val  22363  evl1fval  22371  evl1val  22372  submafval  22619  mdetfval  22626  madufval  22677  minmar1fval  22686  pmatcollpw2lem  22817  pm2mpval  22835  1stcfb  23485  ptbasfi  23621  dfac14  23658  fmval  23983  fmf  23985  flffval  24029  fcfval  24073  cnextval  24101  met1stc  24561  pcoval  25053  iscmet3lem3  25332  rrxsca  25438  mbflimsup  25708  mbflim  25710  itg1climres  25756  mbfi1fseqlem2  25758  mbfi1fseqlem4  25760  mbfi1fseqlem6  25762  mbfi1flimlem  25764  mbfmullem2  25766  itg2monolem1  25792  itg2addlem  25800  itg2cnlem1  25803  cpnfval  25974  mdegfval  26102  elply  26235  plyeq0lem  26250  plypf1  26252  geolim3  26380  ulmuni  26432  ulmcau  26435  ulmdvlem1  26440  ulmdvlem3  26442  mbfulm  26446  itgulm  26448  pserval  26450  dvradcnv  26461  pserdvlem2  26468  abelthlem1  26471  abelthlem3  26473  abelthlem6  26476  logtayl  26702  leibpi  26984  dfef2  27012  emcllem4  27040  emcllem6  27042  emcllem7  27043  lgamgulmlem5  27074  lgamgulmlem6  27075  lgamcvg2  27096  basellem6  27127  sqff1o  27223  dchrptlem2  27306  dchrptlem3  27307  2lgslem1  27435  dchrisumlem3  27532  padicfval  27657  padicabvf  27672  mirval  28801  ishpg  28905  lmif  28931  islmib  28933  axlowdim  29108  crctcshlem3  29965  nmoofval  30911  pjhfval  31545  pjmfn  31864  hosmval  31884  hommval  31885  hodmval  31886  hfsmval  31887  hfmmval  31888  eigvalfval  32046  brafval  32092  kbfval  32101  rnbra  32256  bra11  32257  fpwrelmap  32885  qusima  33555  nsgmgc  33559  nsgqusf1o  33563  idlsrgtset  33665  extvfval  33790  mplvrpmga  33803  esplyval  33820  locfinreflem  34098  rspectopn  34125  zarcmplem  34139  ordtconnlem1  34182  xrhval  34276  sigapildsys  34420  sxbrsigalem2  34544  eulerpart  34640  dstfrvclim1  34736  ballotlemfval  34748  ballotlemsval  34767  signstfv  34821  vtsval  34895  fineqvnttrclse  35384  cvmliftlem5  35603  mrsubffval  35821  mrsubfval  35822  msubffval  35837  msubfval  35838  msubrn  35843  msubco  35845  msubvrs  35874  circum  35988  divcnvlin  36047  climlec3  36048  faclimlem2  36058  faclim2  36062  knoppcnlem1  36895  knoppcnlem6  36900  knoppcnlem7  36901  cnndvlem2  36940  bj-endval  37771  ptrest  38082  poimirlem17  38100  poimirlem20  38103  voliunnfl  38127  volsupnfl  38128  upixp  38192  sdclem2  38205  fdc  38208  lmclim2  38221  geomcau  38222  rrncmslem  38295  pclfvalN  40477  polfvalN  40492  trlset  40749  tendopl  41364  docafvalN  41710  dibfval  41729  dibopelvalN  41731  dibopelval2  41733  dibelval3  41735  dibn0  41741  dib0  41752  diblsmopel  41759  dicn0  41780  dihopelvalcpre  41836  dihatlat  41922  dihpN  41924  dochfval  41938  lcfrlem9  42138  hvmapfval  42347  hvmapval  42348  hdmap1fval  42384  hlhilset  42522  sticksstones10  42736  sticksstones12a  42738  aks6d1c6isolem2  42756  evlselv  43135  prjcrvfval  43177  mzpincl  43279  dfac11  43603  dfac21  43607  hbtlem1  43664  hbtlem7  43666  fsovd  44548  mnringmulrcld  44768  dvgrat  44852  radcnvrat  44854  hashnzfzclim  44862  uzmptshftfval  44886  dvradcnv2  44887  binomcxplemrat  44890  binomcxplemcvg  44894  binomcxplemdvsum  44895  binomcxplemnotnn0  44896  addrval  45005  subrval  45006  mulvval  45007  fmuldfeqlem1  46122  fmuldfeq  46123  clim1fr1  46141  climexp  46145  climneg  46150  climdivf  46152  divcnvg  46167  expfac  46195  climresmpt  46197  climsubmpt  46198  limsupval4  46332  climliminflimsupd  46339  liminfreuzlem  46340  liminfltlem  46342  liminfpnfuz  46354  dvsinax  46451  dvcosax  46464  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvnprodlem1  46484  dvnprodlem2  46485  dvnprodlem3  46486  stoweidlem59  46597  wallispilem5  46607  wallispi  46608  stirlinglem1  46612  stirlinglem8  46619  stirlinglem14  46625  stirlinglem15  46626  dirkerval  46629  fourierdlem71  46715  fourierdlem103  46747  fourierdlem104  46748  fourierdlem112  46756  etransclem48  46820  salgensscntex  46882  sge0tsms  46918  nnfoctbdjlem  46993  isomenndlem  47068  ovnval  47079  ovncvrrp  47102  ovnsubaddlem1  47108  hsphoif  47114  hsphoival  47117  ovnhoilem2  47140  hoidifhspval  47146  ovncvr2  47149  hspmbllem2  47165  vonioolem1  47218  smfpimcclem  47345  smflimsuplem1  47358  smflimsuplem4  47361  smflimsuplem7  47364  smfliminflem  47368  fsupdm  47380  smfsupdmmbllem  47382  finfdm  47384  smfinfdmmbllem  47386  cfsetsnfsetfo  47618  isuspgrim0  48480  cycldlenngric  48514  isgrtri  48529  1aryenef  49231  2aryenef  49242  itcovalpclem2  49257  itcovalt2lem2  49262  ackvalsuc1mpt  49264  ackval0  49266  cofidvala  49701  cofidval  49704  isnatd  49808  swapfelvv  49848  swapf2fvala  49849  swapf1vala  49851  swapf2fn  49853  swapf2vala  49855  tposcurf1  49884  prcofelvv  49965  reldmprcof1  49966  reldmprcof2  49967  prcof1  49973  prcof2a  49974  prcof2  49975  idfudiag1bas  50109  idfudiag1  50110  lmdfval  50234  cmdfval  50235  aacllem  50386