Theorem mptex 7226

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453   ↦ cmpt 5190

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 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545

This theorem is used by:  mptrabex  7228  mptfvmpt  7231  eufnfv  7232  fvresex  7961  ofmres  7985  noinfep  9643  cantnffval  9646  cnfcomlem  9682  cnfcom3clem  9688  ssttrcl  9698  ttrcltr  9699  ttrclselem2  9709  fseqenlem1  10031  dfacacn  10148  dfac12lem1  10150  infmap2  10223  ackbij2lem2  10245  ackbij2lem3  10246  fin23lem32  10350  konigthlem  10581  wunex2  10751  wuncval2  10760  rpnnen1lem1  13032  rpnnen1lem3  13033  rpnnen1lem5  13035  mptnn0fsupp  14065  ccatfn  14641  ccatfval  14642  swrdval  14715  swrd00  14716  swrd0  14732  revval  14833  repsundef  14846  climmpt  15662  climle  15731  iserabs  15906  isumshft  15932  divcnvshft  15948  supcvg  15949  trireciplem  15955  expcnv  15957  explecnv  15958  geolim  15963  geo2lim  15968  cvgrat  15976  mertenslem2  15978  eftlub  16203  rpnnen2lem1  16308  rpnnen2lem2  16309  1arithlem1  17021  1arith  17025  vdwapval  17071  vdwlem6  17084  vdwlem9  17087  restfn  17515  cidffn  17772  idfu2nd  17972  idfu1st  17974  idfucl  17976  fucco  18060  homafval  18124  prf1  18294  prf2fval  18295  prfcl  18297  prf1st  18298  prf2nd  18299  curf1fval  18318  curf11  18320  curf12  18321  curf1cl  18322  curf2  18323  curfcl  18326  hof2val  18350  yonedalem3a  18368  yonedalem4a  18369  yonedalem4b  18370  yonedalem4c  18371  yonedalem3  18374  yonedainv  18375  lubfval  18442  glbfval  18455  smndex1gbasOLD  19018  smndex1gidOLD  19020  smndex1igidOLD  19022  smndex1mnd  19028  smndex1id  19029  smndex1n0mnd  19030  smndex2dbas  19032  smndex2hbas  19034  cntzfval  19453  psgnfval  19633  sylow1lem2  19732  sylow2blem1  19753  sylow2blem2  19754  sylow3lem1  19760  sylow3lem6  19765  pj1fval  19827  vrgpfval  19899  rgspnval  20780  lspfval  21163  sraval  21365  irinitoringc  21698  zrhval2  21727  aspval  22093  psrmulfval  22164  psrass1  22184  mvrval  22202  mplmon  22257  mplcoe1  22259  evlslem2  22301  mpfrcl  22307  evlsval  22308  evlsvvvallem2  22314  evlsvvval  22315  evlsvar  22317  mpfind  22337  selvvvval  22364  mhpfval  22372  psdval  22393  psdmul  22400  coe1fval  22436  psropprmul  22468  coe1mul2  22501  ply1coe  22529  evls1fval  22550  evls1val  22551  evl1fval  22559  evl1val  22560  submafval  22807  mdetfval  22814  madufval  22865  minmar1fval  22874  pmatcollpw2lem  23008  pm2mpval  23026  1stcfb  23676  ptbasfi  23813  dfac14  23850  fmval  24175  fmf  24177  flffval  24221  fcfval  24265  cnextval  24293  met1stc  24753  pcoval  25245  iscmet3lem3  25524  rrxsca  25630  mbflimsup  25900  mbflim  25902  itg1climres  25948  mbfi1fseqlem2  25950  mbfi1fseqlem4  25952  mbfi1fseqlem6  25954  mbfi1flimlem  25956  mbfmullem2  25958  itg2monolem1  25984  itg2addlem  25992  itg2cnlem1  25995  cpnfval  26166  mdegfval  26294  elply  26427  plyeq0lem  26443  plypf1  26445  geolim3  26582  ulmuni  26635  ulmcau  26638  ulmdvlem1  26643  ulmdvlem3  26645  mbfulm  26649  itgulm  26651  pserval  26653  dvradcnv  26664  pserdvlem2  26671  abelthlem1  26674  abelthlem3  26676  abelthlem6  26679  logtayl  26905  leibpi  27187  dfef2  27215  emcllem4  27243  emcllem6  27245  emcllem7  27246  lgamgulmlem5  27277  lgamgulmlem6  27278  lgamcvg2  27299  basellem6  27330  sqff1o  27426  dchrptlem2  27509  dchrptlem3  27510  2lgslem1  27638  dchrisumlem3  27735  padicfval  27860  padicabvf  27875  mirval  29014  ishpg  29124  lmif  29177  islmib  29179  axlowdim  29426  crctcshlem3  30295  nmoofval  31251  pjhfval  31885  pjmfn  32204  hosmval  32224  hommval  32225  hodmval  32226  hfsmval  32227  hfmmval  32228  eigvalfval  32386  brafval  32432  kbfval  32441  rnbra  32596  bra11  32597  fpwrelmap  33212  qusima  33845  nsgmgc  33849  nsgqusf1o  33853  idlsrgtset  33926  extvfval  34050  mplvrpmga  34063  esplyval  34080  locfinreflem  34358  rspectopn  34385  zarcmplem  34399  ordtconnlem1  34442  xrhval  34536  sigapildsys  34681  sxbrsigalem2  34805  eulerpart  34901  dstfrvclim1  34997  ballotlemfval  35009  ballotlemsval  35028  signstfv  35079  vtsval  35153  fineqvnttrclse  35658  cvmliftlem5  35876  mrsubffval  36094  mrsubfval  36095  msubffval  36110  msubfval  36111  msubrn  36116  msubco  36118  msubvrs  36147  circum  36261  divcnvlin  36320  climlec3  36321  faclimlem2  36331  faclim2  36335  knoppcnlem1  37198  knoppcnlem6  37203  knoppcnlem7  37204  cnndvlem2  37243  bj-endval  38075  ptrest  38376  poimirlem17  38394  poimirlem20  38397  voliunnfl  38421  volsupnfl  38422  upixp  38487  sdclem2  38500  fdc  38503  lmclim2  38516  geomcau  38517  rrncmslem  38590  pclfvalN  40770  polfvalN  40785  trlset  41042  tendopl  41657  docafvalN  42003  dibfval  42022  dibopelvalN  42024  dibopelval2  42026  dibelval3  42028  dibn0  42034  dib0  42045  diblsmopel  42052  dicn0  42073  dihopelvalcpre  42129  dihatlat  42215  dihpN  42217  dochfval  42231  lcfrlem9  42431  hvmapfval  42640  hvmapval  42641  hdmap1fval  42677  hlhilset  42815  sticksstones10  43029  sticksstones12a  43031  aks6d1c6isolem2  43049  evlselv  43443  prjcrvfval  43485  mzpincl  43587  dfac11  43911  dfac21  43915  hbtlem1  43972  hbtlem7  43974  fsovd  44856  mnringmulrcld  45074  dvgrat  45144  radcnvrat  45146  hashnzfzclim  45154  uzmptshftfval  45178  dvradcnv2  45179  binomcxplemrat  45182  binomcxplemcvg  45186  binomcxplemdvsum  45187  binomcxplemnotnn0  45188  addrval  45296  subrval  45297  mulvval  45298  fmuldfeqlem1  46420  fmuldfeq  46421  clim1fr1  46439  climexp  46443  climneg  46448  climdivf  46450  divcnvg  46465  expfac  46493  climresmpt  46495  climsubmpt  46496  limsupval4  46630  climliminflimsupd  46637  liminfreuzlem  46638  liminfltlem  46640  liminfpnfuz  46652  dvsinax  46749  dvcosax  46762  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvnprodlem1  46782  dvnprodlem2  46783  dvnprodlem3  46784  stoweidlem59  46895  wallispilem5  46905  wallispi  46906  stirlinglem1  46910  stirlinglem8  46917  stirlinglem14  46923  stirlinglem15  46924  dirkerval  46927  fourierdlem71  47013  fourierdlem103  47045  fourierdlem104  47046  fourierdlem112  47054  etransclem48  47118  salgensscntex  47180  sge0tsms  47216  nnfoctbdjlem  47291  isomenndlem  47366  ovnval  47377  ovncvrrp  47400  ovnsubaddlem1  47406  hsphoif  47412  hsphoival  47415  ovnhoilem2  47438  hoidifhspval  47444  ovncvr2  47447  hspmbllem2  47463  vonioolem1  47516  smfpimcclem  47643  smflimsuplem1  47656  smflimsuplem4  47659  smflimsuplem7  47662  smfliminflem  47666  fsupdm  47678  smfsupdmmbllem  47680  finfdm  47682  smfinfdmmbllem  47684  cfsetsnfsetfo  47956  isuspgrim0  48818  cycldlenngric  48852  isgrtri  48867  1aryenef  49583  2aryenef  49594  itcovalpclem2  49609  itcovalt2lem2  49614  ackvalsuc1mpt  49616  ackval0  49618  cofidvala  50050  cofidval  50053  isnatd  50157  swapfelvv  50197  swapf2fvala  50198  swapf1vala  50200  swapf2fn  50202  swapf2vala  50204  tposcurf1  50233  prcofelvv  50314  reldmprcof1  50315  reldmprcof2  50316  prcof1  50322  prcof2a  50323  prcof2  50324  idfudiag1bas  50458  idfudiag1  50459  lmdfval  50583  cmdfval  50584  aacllem  50780  crosspval  50795  veronesevald  50812