Theorem mptex 7174

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432   ↦ cmpt 5160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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  7176  mptfvmpt  7179  eufnfv  7180  fvresex  7909  ofmres  7933  noinfep  9579  cantnffval  9582  cnfcomlem  9618  cnfcom3clem  9624  ssttrcl  9634  ttrcltr  9635  ttrclselem2  9645  fseqenlem1  9944  dfacacn  10062  dfac12lem1  10064  infmap2  10137  ackbij2lem2  10159  ackbij2lem3  10160  fin23lem32  10264  konigthlem  10489  wunex2  10659  wuncval2  10668  rpnnen1lem1  12926  rpnnen1lem3  12927  rpnnen1lem5  12929  mptnn0fsupp  13957  ccatfn  14532  ccatfval  14533  swrdval  14604  swrd00  14605  swrd0  14619  revval  14720  repsundef  14731  climmpt  15531  climle  15600  iserabs  15776  isumshft  15802  divcnvshft  15818  supcvg  15819  trireciplem  15825  expcnv  15827  explecnv  15828  geolim  15833  geo2lim  15838  cvgrat  15846  mertenslem2  15848  eftlub  16074  rpnnen2lem1  16179  rpnnen2lem2  16180  1arithlem1  16892  1arith  16896  vdwapval  16942  vdwlem6  16955  vdwlem9  16958  restfn  17385  cidffn  17642  idfu2nd  17842  idfu1st  17844  idfucl  17846  fucco  17930  homafval  17994  prf1  18164  prf2fval  18165  prfcl  18167  prf1st  18168  prf2nd  18169  curf1fval  18188  curf11  18190  curf12  18191  curf1cl  18192  curf2  18193  curfcl  18196  hof2val  18220  yonedalem3a  18238  yonedalem4a  18239  yonedalem4b  18240  yonedalem4c  18241  yonedalem3  18244  yonedainv  18245  lubfval  18312  glbfval  18325  smndex1gbasOLD  18869  smndex1gidOLD  18871  smndex1igidOLD  18873  smndex1mnd  18879  smndex1id  18880  smndex1n0mnd  18881  smndex2dbas  18883  smndex2hbas  18885  cntzfval  19293  psgnfval  19473  sylow1lem2  19572  sylow2blem1  19593  sylow2blem2  19594  sylow3lem1  19600  sylow3lem6  19605  pj1fval  19667  vrgpfval  19739  rgspnval  20591  lspfval  20970  sraval  21172  irinitoringc  21461  zrhval2  21490  aspval  21854  psrmulfval  21925  psrass1  21945  mvrval  21963  mplmon  22018  mplcoe1  22020  evlslem2  22062  mpfrcl  22068  evlsval  22069  evlsvvvallem2  22075  evlsvvval  22076  evlsvar  22078  mpfind  22098  selvvvval  22125  mhpfval  22133  psdval  22154  psdmul  22161  coe1fval  22197  psropprmul  22229  coe1mul2  22262  ply1coe  22291  evls1fval  22312  evls1val  22313  evl1fval  22321  evl1val  22322  submafval  22569  mdetfval  22576  madufval  22627  minmar1fval  22636  pmatcollpw2lem  22767  pm2mpval  22785  1stcfb  23435  ptbasfi  23571  dfac14  23608  fmval  23933  fmf  23935  flffval  23979  fcfval  24023  cnextval  24051  met1stc  24511  pcoval  25003  iscmet3lem3  25282  rrxsca  25388  mbflimsup  25658  mbflim  25660  itg1climres  25706  mbfi1fseqlem2  25708  mbfi1fseqlem4  25710  mbfi1fseqlem6  25712  mbfi1flimlem  25714  mbfmullem2  25716  itg2monolem1  25742  itg2addlem  25750  itg2cnlem1  25753  cpnfval  25924  mdegfval  26052  elply  26185  plyeq0lem  26200  plypf1  26202  geolim3  26330  ulmuni  26382  ulmcau  26385  ulmdvlem1  26390  ulmdvlem3  26392  mbfulm  26396  itgulm  26398  pserval  26400  dvradcnv  26411  pserdvlem2  26418  abelthlem1  26421  abelthlem3  26423  abelthlem6  26426  logtayl  26649  leibpi  26931  dfef2  26959  emcllem4  26987  emcllem6  26989  emcllem7  26990  lgamgulmlem5  27021  lgamgulmlem6  27022  lgamcvg2  27043  basellem6  27074  sqff1o  27170  dchrptlem2  27253  dchrptlem3  27254  2lgslem1  27382  dchrisumlem3  27479  padicfval  27604  padicabvf  27619  mirval  28748  ishpg  28852  lmif  28878  islmib  28880  axlowdim  29055  crctcshlem3  29912  nmoofval  30858  pjhfval  31492  pjmfn  31811  hosmval  31831  hommval  31832  hodmval  31833  hfsmval  31834  hfmmval  31835  eigvalfval  31993  brafval  32039  kbfval  32048  rnbra  32203  bra11  32204  fpwrelmap  32832  qusima  33498  nsgmgc  33502  nsgqusf1o  33506  idlsrgtset  33598  extvfval  33723  mplvrpmga  33736  esplyval  33753  locfinreflem  34031  rspectopn  34058  zarcmplem  34072  ordtconnlem1  34115  xrhval  34209  sigapildsys  34353  sxbrsigalem2  34477  eulerpart  34573  dstfrvclim1  34669  ballotlemfval  34681  ballotlemsval  34700  signstfv  34754  vtsval  34828  fineqvnttrclse  35312  cvmliftlem5  35524  mrsubffval  35742  mrsubfval  35743  msubffval  35758  msubfval  35759  msubrn  35764  msubco  35766  msubvrs  35795  circum  35909  divcnvlin  35968  climlec3  35969  faclimlem2  35979  faclim2  35983  knoppcnlem1  36806  knoppcnlem6  36811  knoppcnlem7  36812  cnndvlem2  36851  bj-endval  37682  ptrest  37993  poimirlem17  38011  poimirlem20  38014  voliunnfl  38038  volsupnfl  38039  upixp  38103  sdclem2  38116  fdc  38119  lmclim2  38132  geomcau  38133  rrncmslem  38206  pclfvalN  40388  polfvalN  40403  trlset  40660  tendopl  41275  docafvalN  41621  dibfval  41640  dibopelvalN  41642  dibopelval2  41644  dibelval3  41646  dibn0  41652  dib0  41663  diblsmopel  41670  dicn0  41691  dihopelvalcpre  41747  dihatlat  41833  dihpN  41835  dochfval  41849  lcfrlem9  42049  hvmapfval  42258  hvmapval  42259  hdmap1fval  42295  hlhilset  42433  sticksstones10  42647  sticksstones12a  42649  aks6d1c6isolem2  42667  evlselv  43046  prjcrvfval  43088  mzpincl  43190  dfac11  43514  dfac21  43518  hbtlem1  43575  hbtlem7  43577  fsovd  44459  mnringmulrcld  44679  dvgrat  44763  radcnvrat  44765  hashnzfzclim  44773  uzmptshftfval  44797  dvradcnv2  44798  binomcxplemrat  44801  binomcxplemcvg  44805  binomcxplemdvsum  44806  binomcxplemnotnn0  44807  addrval  44916  subrval  44917  mulvval  44918  fmuldfeqlem1  46034  fmuldfeq  46035  clim1fr1  46053  climexp  46057  climneg  46062  climdivf  46064  divcnvg  46079  expfac  46107  climresmpt  46109  climsubmpt  46110  limsupval4  46244  climliminflimsupd  46251  liminfreuzlem  46252  liminfltlem  46254  liminfpnfuz  46266  dvsinax  46363  dvcosax  46376  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnprodlem1  46396  dvnprodlem2  46397  dvnprodlem3  46398  stoweidlem59  46509  wallispilem5  46519  wallispi  46520  stirlinglem1  46524  stirlinglem8  46531  stirlinglem14  46537  stirlinglem15  46538  dirkerval  46541  fourierdlem71  46627  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  etransclem48  46732  salgensscntex  46794  sge0tsms  46830  nnfoctbdjlem  46905  isomenndlem  46980  ovnval  46991  ovncvrrp  47014  ovnsubaddlem1  47020  hsphoif  47026  hsphoival  47029  ovnhoilem2  47052  hoidifhspval  47058  ovncvr2  47061  hspmbllem2  47077  vonioolem1  47130  smfpimcclem  47257  smflimsuplem1  47270  smflimsuplem4  47273  smflimsuplem7  47276  smfliminflem  47280  fsupdm  47292  smfsupdmmbllem  47294  finfdm  47296  smfinfdmmbllem  47298  cfsetsnfsetfo  47530  isuspgrim0  48392  cycldlenngric  48426  isgrtri  48441  1aryenef  49143  2aryenef  49154  itcovalpclem2  49169  itcovalt2lem2  49174  ackvalsuc1mpt  49176  ackval0  49178  cofidvala  49613  cofidval  49616  isnatd  49720  swapfelvv  49760  swapf2fvala  49761  swapf1vala  49763  swapf2fn  49765  swapf2vala  49767  tposcurf1  49796  prcofelvv  49877  reldmprcof1  49878  reldmprcof2  49879  prcof1  49885  prcof2a  49886  prcof2  49887  idfudiag1bas  50021  idfudiag1  50022  lmdfval  50146  cmdfval  50147  aacllem  50298