Theorem mptex 7221

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539

This theorem is used by:  mptrabex  7223  mptfvmpt  7226  eufnfv  7227  fvresex  7961  ofmres  7985  noinfep  9645  cantnffval  9648  cnfcomlem  9684  cnfcom3clem  9690  ssttrcl  9700  ttrcltr  9701  ttrclselem2  9711  fseqenlem1  10084  dfacacn  10201  dfac12lem1  10203  infmap2  10276  ackbij2lem2  10298  ackbij2lem3  10299  fin23lem32  10403  konigthlem  10634  wunex2  10804  wuncval2  10813  rpnnen1lem1  13087  rpnnen1lem3  13088  rpnnen1lem5  13090  mptnn0fsupp  14120  ccatfn  14697  ccatfval  14698  swrdval  14771  swrd00  14772  swrd0  14788  revval  14889  repsundef  14902  climmpt  15718  climle  15787  iserabs  15962  isumshft  15988  divcnvshft  16004  supcvg  16005  trireciplem  16011  expcnv  16013  explecnv  16014  geolim  16019  geo2lim  16024  cvgrat  16032  mertenslem2  16034  eftlub  16257  rpnnen2lem1  16362  rpnnen2lem2  16363  1arithlem1  17081  1arith  17085  vdwapval  17131  vdwlem6  17144  vdwlem9  17147  restfn  17575  cidffn  17832  idfu2nd  18032  idfu1st  18034  idfucl  18036  fucco  18120  homafval  18184  prf1  18354  prf2fval  18355  prfcl  18357  prf1st  18358  prf2nd  18359  curf1fval  18378  curf11  18380  curf12  18381  curf1cl  18382  curf2  18383  curfcl  18386  hof2val  18410  yonedalem3a  18428  yonedalem4a  18429  yonedalem4b  18430  yonedalem4c  18431  yonedalem3  18434  yonedainv  18435  lubfval  18502  glbfval  18515  smndex1gbasOLD  19079  smndex1gidOLD  19081  smndex1igidOLD  19083  smndex1mnd  19089  smndex1id  19090  smndex1n0mnd  19091  smndex2dbas  19093  smndex2hbas  19095  cntzfval  19514  psgnfval  19694  sylow1lem2  19793  sylow2blem1  19814  sylow2blem2  19815  sylow3lem1  19821  sylow3lem6  19826  pj1fval  19888  vrgpfval  19960  rgspnval  20844  lspfval  21228  sraval  21430  irinitoringc  21765  zrhval2  21794  aspval  22160  psrmulfval  22231  psrass1  22251  mvrval  22269  mplmon  22324  mplcoe1  22326  evlslem2  22368  mpfrcl  22374  evlsval  22375  evlsvvvallem2  22381  evlsvvval  22382  evlsvar  22384  mpfind  22404  selvvvval  22431  mhpfval  22439  psdval  22460  psdmul  22467  coe1fval  22503  psropprmul  22535  coe1mul2  22568  ply1coe  22596  evls1fval  22617  evls1val  22618  evl1fval  22626  evl1val  22627  submafval  22874  mdetfval  22881  madufval  22932  minmar1fval  22941  pmatcollpw2lem  23075  pm2mpval  23093  1stcfb  23743  ptbasfi  23880  dfac14  23917  fmval  24242  fmf  24244  flffval  24288  fcfval  24332  cnextval  24360  met1stc  24820  pcoval  25312  iscmet3lem3  25591  rrxsca  25697  mbflimsup  25967  mbflim  25969  itg1climres  26015  mbfi1fseqlem2  26017  mbfi1fseqlem4  26019  mbfi1fseqlem6  26021  mbfi1flimlem  26023  mbfmullem2  26025  itg2monolem1  26051  itg2addlem  26059  itg2cnlem1  26062  cpnfval  26232  mdegfval  26360  elply  26493  plyeq0lem  26509  plypf1  26511  geolim3  26648  ulmuni  26701  ulmcau  26704  ulmdvlem1  26709  ulmdvlem3  26711  mbfulm  26715  itgulm  26717  pserval  26719  dvradcnv  26730  pserdvlem2  26737  abelthlem1  26740  abelthlem3  26742  abelthlem6  26745  logtayl  26970  leibpi  27252  dfef2  27280  emcllem4  27308  emcllem6  27310  emcllem7  27311  lgamgulmlem5  27342  lgamgulmlem6  27343  lgamcvg2  27364  basellem6  27395  sqff1o  27491  dchrptlem2  27574  dchrptlem3  27575  2lgslem1  27703  dchrisumlem3  27800  padicfval  27925  padicabvf  27940  mirval  29109  ishpg  29219  lmif  29272  islmib  29274  axlowdim  29521  crctcshlem3  30390  nmoofval  31346  pjhfval  31980  pjmfn  32299  hosmval  32319  hommval  32320  hodmval  32321  hfsmval  32322  hfmmval  32323  eigvalfval  32481  brafval  32527  kbfval  32536  rnbra  32691  bra11  32692  fpwrelmap  33307  qusima  33941  nsgmgc  33945  nsgqusf1o  33949  idlsrgtset  34022  extvfval  34146  mplvrpmga  34159  esplyval  34176  locfinreflem  34454  rspectopn  34481  zarcmplem  34495  ordtconnlem1  34538  xrhval  34632  sigapildsys  34777  sxbrsigalem2  34901  eulerpart  34997  dstfrvclim1  35093  ballotlemfval  35105  ballotlemsval  35124  signstfv  35175  vtsval  35249  fineqvnttrclse  35765  cvmliftlem5  36023  mrsubffval  36241  mrsubfval  36242  msubffval  36257  msubfval  36258  msubrn  36263  msubco  36265  msubvrs  36294  circum  36408  divcnvlin  36467  climlec3  36468  faclimlem2  36478  faclim2  36482  knoppcnlem1  37329  knoppcnlem6  37334  knoppcnlem7  37335  cnndvlem2  37374  bj-endval  38204  ptrest  38505  poimirlem17  38523  poimirlem20  38526  voliunnfl  38550  volsupnfl  38551  upixp  38631  sdclem2  38644  fdc  38647  lmclim2  38660  geomcau  38661  rrncmslem  38734  pclfvalN  40914  polfvalN  40929  trlset  41186  tendopl  41801  docafvalN  42147  dibfval  42166  dibopelvalN  42168  dibopelval2  42170  dibelval3  42172  dibn0  42178  dib0  42189  diblsmopel  42196  dicn0  42217  dihopelvalcpre  42273  dihatlat  42359  dihpN  42361  dochfval  42375  lcfrlem9  42575  hvmapfval  42784  hvmapval  42785  hdmap1fval  42821  hlhilset  42959  sticksstones10  43173  sticksstones12a  43175  aks6d1c6isolem2  43193  evlselv  43579  prjcrvfval  43621  mzpincl  43698  dfac11  44022  dfac21  44026  hbtlem1  44083  hbtlem7  44085  fsovd  44967  mnringmulrcld  45185  dvgrat  45255  radcnvrat  45257  hashnzfzclim  45265  uzmptshftfval  45289  dvradcnv2  45290  binomcxplemrat  45293  binomcxplemcvg  45297  binomcxplemdvsum  45298  binomcxplemnotnn0  45299  addrval  45407  subrval  45408  mulvval  45409  fmuldfeqlem1  46538  fmuldfeq  46539  clim1fr1  46557  climexp  46561  climneg  46566  climdivf  46568  divcnvg  46583  expfac  46611  climresmpt  46613  climsubmpt  46614  limsupval4  46748  climliminflimsupd  46755  liminfreuzlem  46756  liminfltlem  46758  liminfpnfuz  46770  dvsinax  46867  dvcosax  46880  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  dvnprodlem1  46900  dvnprodlem2  46901  dvnprodlem3  46902  stoweidlem59  47013  wallispilem5  47023  wallispi  47024  stirlinglem1  47028  stirlinglem8  47035  stirlinglem14  47041  stirlinglem15  47042  dirkerval  47045  fourierdlem71  47131  fourierdlem103  47163  fourierdlem104  47164  fourierdlem112  47172  etransclem48  47236  salgensscntex  47298  sge0tsms  47334  nnfoctbdjlem  47409  isomenndlem  47484  ovnval  47495  ovncvrrp  47518  ovnsubaddlem1  47524  hsphoif  47530  hsphoival  47533  ovnhoilem2  47556  hoidifhspval  47562  ovncvr2  47565  hspmbllem2  47581  vonioolem1  47634  smfpimcclem  47761  smflimsuplem1  47774  smflimsuplem4  47777  smflimsuplem7  47780  smfliminflem  47784  fsupdm  47796  smfsupdmmbllem  47798  finfdm  47800  smfinfdmmbllem  47802  cfsetsnfsetfo  48074  isuspgrim0  48936  cycldlenngric  48970  isgrtri  48985  1aryenef  49701  2aryenef  49712  itcovalpclem2  49727  itcovalt2lem2  49732  ackvalsuc1mpt  49734  ackval0  49736  cofidvala  50168  cofidval  50171  isnatd  50275  swapfelvv  50315  swapf2fvala  50316  swapf1vala  50318  swapf2fn  50320  swapf2vala  50322  tposcurf1  50351  prcofelvv  50432  reldmprcof1  50433  reldmprcof2  50434  prcof1  50440  prcof2a  50441  prcof2  50442  idfudiag1bas  50576  idfudiag1  50577  lmdfval  50701  cmdfval  50702  aacllem  50883  crosspval  50898  veronesevald  50915