Theorem mptex 7178

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429   ↦ cmpt 5166

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506

This theorem is referenced by:  mptrabex  7180  mptfvmpt  7183  eufnfv  7184  fvresex  7913  ofmres  7937  noinfep  9581  cantnffval  9584  cnfcomlem  9620  cnfcom3clem  9626  ssttrcl  9636  ttrcltr  9637  ttrclselem2  9647  fseqenlem1  9946  dfacacn  10064  dfac12lem1  10066  infmap2  10139  ackbij2lem2  10161  ackbij2lem3  10162  fin23lem32  10266  konigthlem  10491  wunex2  10661  wuncval2  10670  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  mptnn0fsupp  13959  ccatfn  14534  ccatfval  14535  swrdval  14606  swrd00  14607  swrd0  14621  revval  14722  repsundef  14733  climmpt  15533  climle  15602  iserabs  15778  isumshft  15804  divcnvshft  15820  supcvg  15821  trireciplem  15827  expcnv  15829  explecnv  15830  geolim  15835  geo2lim  15840  cvgrat  15848  mertenslem2  15850  eftlub  16076  rpnnen2lem1  16181  rpnnen2lem2  16182  1arithlem1  16894  1arith  16898  vdwapval  16944  vdwlem6  16957  vdwlem9  16960  restfn  17387  cidffn  17644  idfu2nd  17844  idfu1st  17846  idfucl  17848  fucco  17932  homafval  17996  prf1  18166  prf2fval  18167  prfcl  18169  prf1st  18170  prf2nd  18171  curf1fval  18190  curf11  18192  curf12  18193  curf1cl  18194  curf2  18195  curfcl  18198  hof2val  18222  yonedalem3a  18240  yonedalem4a  18241  yonedalem4b  18242  yonedalem4c  18243  yonedalem3  18246  yonedainv  18247  lubfval  18314  glbfval  18327  smndex1gbasOLD  18871  smndex1gidOLD  18873  smndex1igidOLD  18875  smndex1mnd  18881  smndex1id  18882  smndex1n0mnd  18883  smndex2dbas  18885  smndex2hbas  18887  cntzfval  19295  psgnfval  19475  sylow1lem2  19574  sylow2blem1  19595  sylow2blem2  19596  sylow3lem1  19602  sylow3lem6  19607  pj1fval  19669  vrgpfval  19741  rgspnval  20589  lspfval  20968  sraval  21170  irinitoringc  21459  zrhval2  21488  aspval  21852  psrmulfval  21922  psrass1  21942  mvrval  21960  mplmon  22013  mplcoe1  22015  evlslem2  22057  mpfrcl  22063  evlsval  22064  evlsvvvallem2  22070  evlsvvval  22071  evlsvar  22073  mpfind  22093  mhpfval  22104  psdval  22125  psdmul  22132  coe1fval  22169  psropprmul  22201  coe1mul2  22234  ply1coe  22263  evls1fval  22284  evls1val  22285  evl1fval  22293  evl1val  22294  submafval  22544  mdetfval  22551  madufval  22602  minmar1fval  22611  pmatcollpw2lem  22742  pm2mpval  22760  1stcfb  23410  ptbasfi  23546  dfac14  23583  fmval  23908  fmf  23910  flffval  23954  fcfval  23998  cnextval  24026  met1stc  24486  pcoval  24978  iscmet3lem3  25257  rrxsca  25363  mbflimsup  25633  mbflim  25635  itg1climres  25681  mbfi1fseqlem2  25683  mbfi1fseqlem4  25685  mbfi1fseqlem6  25687  mbfi1flimlem  25689  mbfmullem2  25691  itg2monolem1  25717  itg2addlem  25725  itg2cnlem1  25728  cpnfval  25899  mdegfval  26027  elply  26160  plyeq0lem  26175  plypf1  26177  geolim3  26305  ulmuni  26357  ulmcau  26360  ulmdvlem1  26365  ulmdvlem3  26367  mbfulm  26371  itgulm  26373  pserval  26375  dvradcnv  26386  pserdvlem2  26393  abelthlem1  26396  abelthlem3  26398  abelthlem6  26401  logtayl  26624  leibpi  26906  dfef2  26934  emcllem4  26962  emcllem6  26964  emcllem7  26965  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamcvg2  27018  basellem6  27049  sqff1o  27145  dchrptlem2  27228  dchrptlem3  27229  2lgslem1  27357  dchrisumlem3  27454  padicfval  27579  padicabvf  27594  mirval  28723  ishpg  28827  lmif  28853  islmib  28855  axlowdim  29030  crctcshlem3  29887  nmoofval  30833  pjhfval  31467  pjmfn  31786  hosmval  31806  hommval  31807  hodmval  31808  hfsmval  31809  hfmmval  31810  eigvalfval  31968  brafval  32014  kbfval  32023  rnbra  32178  bra11  32179  fpwrelmap  32806  qusima  33468  nsgmgc  33472  nsgqusf1o  33476  idlsrgtset  33568  extvfval  33676  mplvrpmga  33689  esplyval  33706  locfinreflem  33984  rspectopn  34011  zarcmplem  34025  ordtconnlem1  34068  xrhval  34162  sigapildsys  34306  sxbrsigalem2  34430  eulerpart  34526  dstfrvclim1  34622  ballotlemfval  34634  ballotlemsval  34653  signstfv  34707  vtsval  34781  fineqvnttrclse  35268  cvmliftlem5  35471  mrsubffval  35689  mrsubfval  35690  msubffval  35705  msubfval  35706  msubrn  35711  msubco  35713  msubvrs  35742  circum  35856  divcnvlin  35915  climlec3  35916  faclimlem2  35926  faclim2  35930  knoppcnlem1  36753  knoppcnlem6  36758  knoppcnlem7  36759  cnndvlem2  36798  bj-endval  37629  ptrest  37940  poimirlem17  37958  poimirlem20  37961  voliunnfl  37985  volsupnfl  37986  upixp  38050  sdclem2  38063  fdc  38066  lmclim2  38079  geomcau  38080  rrncmslem  38153  pclfvalN  40335  polfvalN  40350  trlset  40607  tendopl  41222  docafvalN  41568  dibfval  41587  dibopelvalN  41589  dibopelval2  41591  dibelval3  41593  dibn0  41599  dib0  41610  diblsmopel  41617  dicn0  41638  dihopelvalcpre  41694  dihatlat  41780  dihpN  41782  dochfval  41796  lcfrlem9  41996  hvmapfval  42205  hvmapval  42206  hdmap1fval  42242  hlhilset  42380  sticksstones10  42594  sticksstones12a  42596  aks6d1c6isolem2  42614  selvvvval  43018  evlselv  43020  prjcrvfval  43064  mzpincl  43166  dfac11  43490  dfac21  43494  hbtlem1  43551  hbtlem7  43553  fsovd  44435  mnringmulrcld  44655  dvgrat  44739  radcnvrat  44741  hashnzfzclim  44749  uzmptshftfval  44773  dvradcnv2  44774  binomcxplemrat  44777  binomcxplemcvg  44781  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  addrval  44892  subrval  44893  mulvval  44894  fmuldfeqlem1  46012  fmuldfeq  46013  clim1fr1  46031  climexp  46035  climneg  46040  climdivf  46042  divcnvg  46057  expfac  46085  climresmpt  46087  climsubmpt  46088  limsupval4  46222  climliminflimsupd  46229  liminfreuzlem  46230  liminfltlem  46232  liminfpnfuz  46244  dvsinax  46341  dvcosax  46354  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  stoweidlem59  46487  wallispilem5  46497  wallispi  46498  stirlinglem1  46502  stirlinglem8  46509  stirlinglem14  46515  stirlinglem15  46516  dirkerval  46519  fourierdlem71  46605  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  etransclem48  46710  salgensscntex  46772  sge0tsms  46808  nnfoctbdjlem  46883  isomenndlem  46958  ovnval  46969  ovncvrrp  46992  ovnsubaddlem1  46998  hsphoif  47004  hsphoival  47007  ovnhoilem2  47030  hoidifhspval  47036  ovncvr2  47039  hspmbllem2  47055  vonioolem1  47108  smfpimcclem  47235  smflimsuplem1  47248  smflimsuplem4  47251  smflimsuplem7  47254  smfliminflem  47258  fsupdm  47270  smfsupdmmbllem  47272  finfdm  47274  smfinfdmmbllem  47276  cfsetsnfsetfo  47508  isuspgrim0  48370  cycldlenngric  48404  isgrtri  48419  1aryenef  49121  2aryenef  49132  itcovalpclem2  49147  itcovalt2lem2  49152  ackvalsuc1mpt  49154  ackval0  49156  cofidvala  49591  cofidval  49594  isnatd  49698  swapfelvv  49738  swapf2fvala  49739  swapf1vala  49741  swapf2fn  49743  swapf2vala  49745  tposcurf1  49774  prcofelvv  49855  reldmprcof1  49856  reldmprcof2  49857  prcof1  49863  prcof2a  49864  prcof2  49865  idfudiag1bas  49999  idfudiag1  50000  lmdfval  50124  cmdfval  50125  aacllem  50276