Theorem mptex 7171

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430   ↦ cmpt 5167

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 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pr 5370

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  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  7173  mptfvmpt  7176  eufnfv  7177  fvresex  7906  ofmres  7930  noinfep  9572  cantnffval  9575  cnfcomlem  9611  cnfcom3clem  9617  ssttrcl  9627  ttrcltr  9628  ttrclselem2  9638  fseqenlem1  9937  dfacacn  10055  dfac12lem1  10057  infmap2  10130  ackbij2lem2  10152  ackbij2lem3  10153  fin23lem32  10257  konigthlem  10482  wunex2  10652  wuncval2  10661  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  mptnn0fsupp  13950  ccatfn  14525  ccatfval  14526  swrdval  14597  swrd00  14598  swrd0  14612  revval  14713  repsundef  14724  climmpt  15524  climle  15593  iserabs  15769  isumshft  15795  divcnvshft  15811  supcvg  15812  trireciplem  15818  expcnv  15820  explecnv  15821  geolim  15826  geo2lim  15831  cvgrat  15839  mertenslem2  15841  eftlub  16067  rpnnen2lem1  16172  rpnnen2lem2  16173  1arithlem1  16885  1arith  16889  vdwapval  16935  vdwlem6  16948  vdwlem9  16951  restfn  17378  cidffn  17635  idfu2nd  17835  idfu1st  17837  idfucl  17839  fucco  17923  homafval  17987  prf1  18157  prf2fval  18158  prfcl  18160  prf1st  18161  prf2nd  18162  curf1fval  18181  curf11  18183  curf12  18184  curf1cl  18185  curf2  18186  curfcl  18189  hof2val  18213  yonedalem3a  18231  yonedalem4a  18232  yonedalem4b  18233  yonedalem4c  18234  yonedalem3  18237  yonedainv  18238  lubfval  18305  glbfval  18318  smndex1gbasOLD  18862  smndex1gidOLD  18864  smndex1igidOLD  18866  smndex1mnd  18872  smndex1id  18873  smndex1n0mnd  18874  smndex2dbas  18876  smndex2hbas  18878  cntzfval  19286  psgnfval  19466  sylow1lem2  19565  sylow2blem1  19586  sylow2blem2  19587  sylow3lem1  19593  sylow3lem6  19598  pj1fval  19660  vrgpfval  19732  rgspnval  20580  lspfval  20959  sraval  21162  irinitoringc  21469  zrhval2  21498  aspval  21862  psrmulfval  21932  psrass1  21952  mvrval  21970  mplmon  22023  mplcoe1  22025  evlslem2  22067  mpfrcl  22073  evlsval  22074  evlsvvvallem2  22080  evlsvvval  22081  evlsvar  22083  mpfind  22103  mhpfval  22114  psdval  22135  psdmul  22142  coe1fval  22179  psropprmul  22211  coe1mul2  22244  ply1coe  22273  evls1fval  22294  evls1val  22295  evl1fval  22303  evl1val  22304  submafval  22554  mdetfval  22561  madufval  22612  minmar1fval  22621  pmatcollpw2lem  22752  pm2mpval  22770  1stcfb  23420  ptbasfi  23556  dfac14  23593  fmval  23918  fmf  23920  flffval  23964  fcfval  24008  cnextval  24036  met1stc  24496  pcoval  24988  iscmet3lem3  25267  rrxsca  25373  mbflimsup  25643  mbflim  25645  itg1climres  25691  mbfi1fseqlem2  25693  mbfi1fseqlem4  25695  mbfi1fseqlem6  25697  mbfi1flimlem  25699  mbfmullem2  25701  itg2monolem1  25727  itg2addlem  25735  itg2cnlem1  25738  cpnfval  25909  mdegfval  26037  elply  26170  plyeq0lem  26185  plypf1  26187  geolim3  26316  ulmuni  26370  ulmcau  26373  ulmdvlem1  26378  ulmdvlem3  26380  mbfulm  26384  itgulm  26386  pserval  26388  dvradcnv  26399  pserdvlem2  26406  abelthlem1  26409  abelthlem3  26411  abelthlem6  26414  logtayl  26637  leibpi  26919  dfef2  26948  emcllem4  26976  emcllem6  26978  emcllem7  26979  lgamgulmlem5  27010  lgamgulmlem6  27011  lgamcvg2  27032  basellem6  27063  sqff1o  27159  dchrptlem2  27242  dchrptlem3  27243  2lgslem1  27371  dchrisumlem3  27468  padicfval  27593  padicabvf  27608  mirval  28737  ishpg  28841  lmif  28867  islmib  28869  axlowdim  29044  crctcshlem3  29902  nmoofval  30848  pjhfval  31482  pjmfn  31801  hosmval  31821  hommval  31822  hodmval  31823  hfsmval  31824  hfmmval  31825  eigvalfval  31983  brafval  32029  kbfval  32038  rnbra  32193  bra11  32194  fpwrelmap  32821  qusima  33483  nsgmgc  33487  nsgqusf1o  33491  idlsrgtset  33583  extvfval  33691  mplvrpmga  33704  esplyval  33721  locfinreflem  34000  rspectopn  34027  zarcmplem  34041  ordtconnlem1  34084  xrhval  34178  sigapildsys  34322  sxbrsigalem2  34446  eulerpart  34542  dstfrvclim1  34638  ballotlemfval  34650  ballotlemsval  34669  signstfv  34723  vtsval  34797  fineqvnttrclse  35284  cvmliftlem5  35487  mrsubffval  35705  mrsubfval  35706  msubffval  35721  msubfval  35722  msubrn  35727  msubco  35729  msubvrs  35758  circum  35872  divcnvlin  35931  climlec3  35932  faclimlem2  35942  faclim2  35946  knoppcnlem1  36769  knoppcnlem6  36774  knoppcnlem7  36775  cnndvlem2  36814  bj-endval  37645  ptrest  37954  poimirlem17  37972  poimirlem20  37975  voliunnfl  37999  volsupnfl  38000  upixp  38064  sdclem2  38077  fdc  38080  lmclim2  38093  geomcau  38094  rrncmslem  38167  pclfvalN  40349  polfvalN  40364  trlset  40621  tendopl  41236  docafvalN  41582  dibfval  41601  dibopelvalN  41603  dibopelval2  41605  dibelval3  41607  dibn0  41613  dib0  41624  diblsmopel  41631  dicn0  41652  dihopelvalcpre  41708  dihatlat  41794  dihpN  41796  dochfval  41810  lcfrlem9  42010  hvmapfval  42219  hvmapval  42220  hdmap1fval  42256  hlhilset  42394  sticksstones10  42608  sticksstones12a  42610  aks6d1c6isolem2  42628  selvvvval  43032  evlselv  43034  prjcrvfval  43078  mzpincl  43180  dfac11  43508  dfac21  43512  hbtlem1  43569  hbtlem7  43571  fsovd  44453  mnringmulrcld  44673  dvgrat  44757  radcnvrat  44759  hashnzfzclim  44767  uzmptshftfval  44791  dvradcnv2  44792  binomcxplemrat  44795  binomcxplemcvg  44799  binomcxplemdvsum  44800  binomcxplemnotnn0  44801  addrval  44910  subrval  44911  mulvval  44912  fmuldfeqlem1  46030  fmuldfeq  46031  clim1fr1  46049  climexp  46053  climneg  46058  climdivf  46060  divcnvg  46075  expfac  46103  climresmpt  46105  climsubmpt  46106  limsupval4  46240  climliminflimsupd  46247  liminfreuzlem  46248  liminfltlem  46250  liminfpnfuz  46262  dvsinax  46359  dvcosax  46372  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnprodlem1  46392  dvnprodlem2  46393  dvnprodlem3  46394  stoweidlem59  46505  wallispilem5  46515  wallispi  46516  stirlinglem1  46520  stirlinglem8  46527  stirlinglem14  46533  stirlinglem15  46534  dirkerval  46537  fourierdlem71  46623  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  etransclem48  46728  salgensscntex  46790  sge0tsms  46826  nnfoctbdjlem  46901  isomenndlem  46976  ovnval  46987  ovncvrrp  47010  ovnsubaddlem1  47016  hsphoif  47022  hsphoival  47025  ovnhoilem2  47048  hoidifhspval  47054  ovncvr2  47057  hspmbllem2  47073  vonioolem1  47126  smfpimcclem  47253  smflimsuplem1  47266  smflimsuplem4  47269  smflimsuplem7  47272  smfliminflem  47276  fsupdm  47288  smfsupdmmbllem  47290  finfdm  47292  smfinfdmmbllem  47294  cfsetsnfsetfo  47520  isuspgrim0  48382  cycldlenngric  48416  isgrtri  48431  1aryenef  49133  2aryenef  49144  itcovalpclem2  49159  itcovalt2lem2  49164  ackvalsuc1mpt  49166  ackval0  49168  cofidvala  49603  cofidval  49606  isnatd  49710  swapfelvv  49750  swapf2fvala  49751  swapf1vala  49753  swapf2fn  49755  swapf2vala  49757  tposcurf1  49786  prcofelvv  49867  reldmprcof1  49868  reldmprcof2  49869  prcof1  49875  prcof2a  49876  prcof2  49877  idfudiag1bas  50011  idfudiag1  50012  lmdfval  50136  cmdfval  50137  aacllem  50288