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 2106  Vcvv 3446   ↦ cmpt 5193

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509

This theorem is referenced by:  mptrabex  7180  mptfvmpt  7183  eufnfv  7184  fvresex  7897  ofmres  7922  noinfep  9605  cantnffval  9608  cnfcomlem  9644  cnfcom3clem  9650  ssttrcl  9660  ttrcltr  9661  ttrclselem2  9671  fseqenlem1  9969  dfacacn  10086  dfac12lem1  10088  infmap2  10163  ackbij2lem2  10185  ackbij2lem3  10186  fin23lem32  10289  konigthlem  10513  wunex2  10683  wuncval2  10692  rpnnen1lem1  12912  rpnnen1lem3  12913  rpnnen1lem5  12915  mptnn0fsupp  13912  ccatfn  14472  ccatfval  14473  swrdval  14543  swrd00  14544  swrd0  14558  revval  14660  repsundef  14671  climmpt  15465  climle  15534  iserabs  15711  isumshft  15735  divcnvshft  15751  supcvg  15752  trireciplem  15758  expcnv  15760  explecnv  15761  geolim  15766  geo2lim  15771  cvgrat  15779  mertenslem2  15781  eftlub  16002  rpnnen2lem1  16107  rpnnen2lem2  16108  1arithlem1  16806  1arith  16810  vdwapval  16856  vdwlem6  16869  vdwlem9  16872  restfn  17320  cidffn  17572  idfu2nd  17777  idfu1st  17779  idfucl  17781  fucco  17865  homafval  17929  prf1  18102  prf2fval  18103  prfcl  18105  prf1st  18106  prf2nd  18107  curf1fval  18127  curf11  18129  curf12  18130  curf1cl  18131  curf2  18132  curfcl  18135  hof2val  18159  yonedalem3a  18177  yonedalem4a  18178  yonedalem4b  18179  yonedalem4c  18180  yonedalem3  18183  yonedainv  18184  lubfval  18253  glbfval  18266  smndex1gbas  18726  smndex1gid  18727  smndex1igid  18728  smndex1mnd  18734  smndex1id  18735  smndex1n0mnd  18736  smndex2dbas  18738  smndex2hbas  18740  cntzfval  19114  psgnfval  19296  sylow1lem2  19395  sylow2blem1  19416  sylow2blem2  19417  sylow3lem1  19423  sylow3lem6  19428  pj1fval  19490  vrgpfval  19562  lspfval  20491  sraval  20696  zrhval2  20946  aspval  21313  psrmulfval  21390  psrass1  21411  mvrval  21427  mplmon  21473  mplcoe1  21475  evlslem2  21526  mpfrcl  21532  evlsval  21533  evlsvar  21537  mpfind  21554  mhpfval  21566  coe1fval  21613  psropprmul  21646  coe1mul2  21677  ply1coe  21704  evls1fval  21722  evls1val  21723  evl1fval  21731  evl1val  21732  submafval  21965  mdetfval  21972  madufval  22023  minmar1fval  22032  pmatcollpw2lem  22163  pm2mpval  22181  1stcfb  22833  ptbasfi  22969  dfac14  23006  fmval  23331  fmf  23333  flffval  23377  fcfval  23421  cnextval  23449  met1stc  23914  pcoval  24411  iscmet3lem3  24691  rrxsca  24797  mbflimsup  25067  mbflim  25069  itg1climres  25116  mbfi1fseqlem2  25118  mbfi1fseqlem4  25120  mbfi1fseqlem6  25122  mbfi1flimlem  25124  mbfmullem2  25126  itg2monolem1  25152  itg2addlem  25160  itg2cnlem1  25163  cpnfval  25333  mdegfval  25464  elply  25593  plyeq0lem  25608  plypf1  25610  geolim3  25736  ulmuni  25788  ulmcau  25791  ulmdvlem1  25796  ulmdvlem3  25798  mbfulm  25802  itgulm  25804  pserval  25806  dvradcnv  25817  pserdvlem2  25824  abelthlem1  25827  abelthlem3  25829  abelthlem6  25832  logtayl  26052  leibpi  26329  dfef2  26357  emcllem4  26385  emcllem6  26387  emcllem7  26388  lgamgulmlem5  26419  lgamgulmlem6  26420  lgamcvg2  26441  basellem6  26472  sqff1o  26568  dchrptlem2  26650  dchrptlem3  26651  2lgslem1  26779  dchrisumlem3  26876  padicfval  27001  padicabvf  27016  istrkg2ld  27465  mirval  27660  ishpg  27764  lmif  27790  islmib  27792  axlowdim  27973  crctcshlem3  28827  nmoofval  29767  pjhfval  30401  pjmfn  30720  hosmval  30740  hommval  30741  hodmval  30742  hfsmval  30743  hfmmval  30744  eigvalfval  30902  brafval  30948  kbfval  30957  rnbra  31112  bra11  31113  padct  31704  fpwrelmap  31718  qusima  32261  nsgmgc  32264  nsgqusf1o  32268  idlsrgtset  32326  locfinreflem  32510  rspectopn  32537  zarcmplem  32551  ordtconnlem1  32594  xrhval  32688  sigapildsys  32850  sxbrsigalem2  32975  eulerpart  33071  dstfrvclim1  33166  ballotlemfval  33178  ballotlemsval  33197  signstfv  33264  vtsval  33339  cvmliftlem5  33970  mrsubffval  34188  mrsubfval  34189  msubffval  34204  msubfval  34205  msubrn  34210  msubco  34212  msubvrs  34241  circum  34349  divcnvlin  34391  climlec3  34392  faclimlem2  34403  faclim2  34407  knoppcnlem1  35032  knoppcnlem6  35037  knoppcnlem7  35038  cnndvlem2  35077  bj-endval  35859  ptrest  36150  poimirlem17  36168  poimirlem20  36171  voliunnfl  36195  volsupnfl  36196  upixp  36261  sdclem2  36274  fdc  36277  lmclim2  36290  geomcau  36291  rrncmslem  36364  pclfvalN  38425  polfvalN  38440  trlset  38697  tendopl  39312  docafvalN  39658  dibfval  39677  dibopelvalN  39679  dibopelval2  39681  dibelval3  39683  dibn0  39689  dib0  39700  diblsmopel  39707  dicn0  39728  dihopelvalcpre  39784  dihatlat  39870  dihpN  39872  dochfval  39886  lcfrlem9  40086  hvmapfval  40295  hvmapval  40296  hdmap1fval  40332  hlhilset  40470  sticksstones10  40636  sticksstones12a  40638  evlsbagval  40806  mhphf  40829  prjcrvfval  41027  mzpincl  41115  dfac11  41447  dfac21  41451  hbtlem1  41508  hbtlem7  41510  rgspnval  41553  fsovd  42402  mnringmulrcld  42630  dvgrat  42714  radcnvrat  42716  hashnzfzclim  42724  uzmptshftfval  42748  dvradcnv2  42749  binomcxplemrat  42752  binomcxplemcvg  42756  binomcxplemdvsum  42757  binomcxplemnotnn0  42758  addrval  42868  subrval  42869  mulvval  42870  fmuldfeqlem1  43943  fmuldfeq  43944  clim1fr1  43962  climexp  43966  climneg  43971  climdivf  43973  divcnvg  43988  expfac  44018  climresmpt  44020  climsubmpt  44021  limsupval4  44155  climliminflimsupd  44162  liminfreuzlem  44163  liminfltlem  44165  liminfpnfuz  44177  dvsinax  44274  dvcosax  44287  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  dvnprodlem1  44307  dvnprodlem2  44308  dvnprodlem3  44309  stoweidlem59  44420  wallispilem5  44430  wallispi  44431  stirlinglem1  44435  stirlinglem8  44442  stirlinglem14  44448  stirlinglem15  44449  dirkerval  44452  fourierdlem71  44538  fourierdlem103  44570  fourierdlem104  44571  fourierdlem112  44579  etransclem48  44643  salgensscntex  44705  sge0tsms  44741  nnfoctbdjlem  44816  isomenndlem  44891  ovnval  44902  ovncvrrp  44925  ovnsubaddlem1  44931  hsphoif  44937  hsphoival  44940  ovnhoilem2  44963  hoidifhspval  44969  ovncvr2  44972  hspmbllem2  44988  vonioolem1  45041  smfpimcclem  45168  smflimsuplem1  45181  smflimsuplem4  45184  smflimsuplem7  45187  smfliminflem  45191  fsupdm  45203  smfsupdmmbllem  45205  finfdm  45207  smfinfdmmbllem  45209  cfsetsnfsetfo  45414  isomuspgrlem2  46145  irinitoringc  46487  1aryenef  46851  2aryenef  46862  itcovalpclem2  46877  itcovalt2lem2  46882  ackvalsuc1mpt  46884  ackval0  46886  aacllem  47368