Theorem mptex 7197

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447   ↦ cmpt 5188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  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 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519

This theorem is referenced by:  mptrabex  7199  mptfvmpt  7202  eufnfv  7203  fvresex  7938  ofmres  7963  noinfep  9613  cantnffval  9616  cnfcomlem  9652  cnfcom3clem  9658  ssttrcl  9668  ttrcltr  9669  ttrclselem2  9679  fseqenlem1  9977  dfacacn  10095  dfac12lem1  10097  infmap2  10170  ackbij2lem2  10192  ackbij2lem3  10193  fin23lem32  10297  konigthlem  10521  wunex2  10691  wuncval2  10700  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  mptnn0fsupp  13962  ccatfn  14537  ccatfval  14538  swrdval  14608  swrd00  14609  swrd0  14623  revval  14725  repsundef  14736  climmpt  15537  climle  15606  iserabs  15781  isumshft  15805  divcnvshft  15821  supcvg  15822  trireciplem  15828  expcnv  15830  explecnv  15831  geolim  15836  geo2lim  15841  cvgrat  15849  mertenslem2  15851  eftlub  16077  rpnnen2lem1  16182  rpnnen2lem2  16183  1arithlem1  16894  1arith  16898  vdwapval  16944  vdwlem6  16957  vdwlem9  16960  restfn  17387  cidffn  17639  idfu2nd  17839  idfu1st  17841  idfucl  17843  fucco  17927  homafval  17991  prf1  18161  prf2fval  18162  prfcl  18164  prf1st  18165  prf2nd  18166  curf1fval  18185  curf11  18187  curf12  18188  curf1cl  18189  curf2  18190  curfcl  18193  hof2val  18217  yonedalem3a  18235  yonedalem4a  18236  yonedalem4b  18237  yonedalem4c  18238  yonedalem3  18241  yonedainv  18242  lubfval  18309  glbfval  18322  smndex1gbas  18829  smndex1gid  18830  smndex1igid  18831  smndex1mnd  18837  smndex1id  18838  smndex1n0mnd  18839  smndex2dbas  18841  smndex2hbas  18843  cntzfval  19252  psgnfval  19430  sylow1lem2  19529  sylow2blem1  19550  sylow2blem2  19551  sylow3lem1  19557  sylow3lem6  19562  pj1fval  19624  vrgpfval  19696  rgspnval  20521  lspfval  20879  sraval  21082  irinitoringc  21389  zrhval2  21418  aspval  21782  psrmulfval  21852  psrass1  21873  mvrval  21891  mplmon  21942  mplcoe1  21944  evlslem2  21986  mpfrcl  21992  evlsval  21993  evlsvar  21997  mpfind  22014  mhpfval  22025  psdval  22046  psdmul  22053  coe1fval  22090  psropprmul  22122  coe1mul2  22155  ply1coe  22185  evls1fval  22206  evls1val  22207  evl1fval  22215  evl1val  22216  submafval  22466  mdetfval  22473  madufval  22524  minmar1fval  22533  pmatcollpw2lem  22664  pm2mpval  22682  1stcfb  23332  ptbasfi  23468  dfac14  23505  fmval  23830  fmf  23832  flffval  23876  fcfval  23920  cnextval  23948  met1stc  24409  pcoval  24911  iscmet3lem3  25190  rrxsca  25296  mbflimsup  25567  mbflim  25569  itg1climres  25615  mbfi1fseqlem2  25617  mbfi1fseqlem4  25619  mbfi1fseqlem6  25621  mbfi1flimlem  25623  mbfmullem2  25625  itg2monolem1  25651  itg2addlem  25659  itg2cnlem1  25662  cpnfval  25834  mdegfval  25967  elply  26100  plyeq0lem  26115  plypf1  26117  geolim3  26247  ulmuni  26301  ulmcau  26304  ulmdvlem1  26309  ulmdvlem3  26311  mbfulm  26315  itgulm  26317  pserval  26319  dvradcnv  26330  pserdvlem2  26338  abelthlem1  26341  abelthlem3  26343  abelthlem6  26346  logtayl  26569  leibpi  26852  dfef2  26881  emcllem4  26909  emcllem6  26911  emcllem7  26912  lgamgulmlem5  26943  lgamgulmlem6  26944  lgamcvg2  26965  basellem6  26996  sqff1o  27092  dchrptlem2  27176  dchrptlem3  27177  2lgslem1  27305  dchrisumlem3  27402  padicfval  27527  padicabvf  27542  istrkg2ld  28387  mirval  28582  ishpg  28686  lmif  28712  islmib  28714  axlowdim  28888  crctcshlem3  29749  nmoofval  30691  pjhfval  31325  pjmfn  31644  hosmval  31664  hommval  31665  hodmval  31666  hfsmval  31667  hfmmval  31668  eigvalfval  31826  brafval  31872  kbfval  31881  rnbra  32036  bra11  32037  padct  32643  fpwrelmap  32656  qusima  33379  nsgmgc  33383  nsgqusf1o  33387  idlsrgtset  33479  locfinreflem  33830  rspectopn  33857  zarcmplem  33871  ordtconnlem1  33914  xrhval  34008  sigapildsys  34152  sxbrsigalem2  34277  eulerpart  34373  dstfrvclim1  34469  ballotlemfval  34481  ballotlemsval  34500  signstfv  34554  vtsval  34628  cvmliftlem5  35276  mrsubffval  35494  mrsubfval  35495  msubffval  35510  msubfval  35511  msubrn  35516  msubco  35518  msubvrs  35547  circum  35661  divcnvlin  35720  climlec3  35721  faclimlem2  35731  faclim2  35735  knoppcnlem1  36481  knoppcnlem6  36486  knoppcnlem7  36487  cnndvlem2  36526  bj-endval  37303  ptrest  37613  poimirlem17  37631  poimirlem20  37634  voliunnfl  37658  volsupnfl  37659  upixp  37723  sdclem2  37736  fdc  37739  lmclim2  37752  geomcau  37753  rrncmslem  37826  pclfvalN  39883  polfvalN  39898  trlset  40155  tendopl  40770  docafvalN  41116  dibfval  41135  dibopelvalN  41137  dibopelval2  41139  dibelval3  41141  dibn0  41147  dib0  41158  diblsmopel  41165  dicn0  41186  dihopelvalcpre  41242  dihatlat  41328  dihpN  41330  dochfval  41344  lcfrlem9  41544  hvmapfval  41753  hvmapval  41754  hdmap1fval  41790  hlhilset  41928  sticksstones10  42143  sticksstones12a  42145  aks6d1c6isolem2  42163  evlsvvvallem2  42550  evlsvvval  42551  selvvvval  42573  evlselv  42575  prjcrvfval  42619  mzpincl  42722  dfac11  43051  dfac21  43055  hbtlem1  43112  hbtlem7  43114  fsovd  43997  mnringmulrcld  44217  dvgrat  44301  radcnvrat  44303  hashnzfzclim  44311  uzmptshftfval  44335  dvradcnv2  44336  binomcxplemrat  44339  binomcxplemcvg  44343  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  addrval  44455  subrval  44456  mulvval  44457  fmuldfeqlem1  45580  fmuldfeq  45581  clim1fr1  45599  climexp  45603  climneg  45608  climdivf  45610  divcnvg  45625  expfac  45655  climresmpt  45657  climsubmpt  45658  limsupval4  45792  climliminflimsupd  45799  liminfreuzlem  45800  liminfltlem  45802  liminfpnfuz  45814  dvsinax  45911  dvcosax  45924  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  stoweidlem59  46057  wallispilem5  46067  wallispi  46068  stirlinglem1  46072  stirlinglem8  46079  stirlinglem14  46085  stirlinglem15  46086  dirkerval  46089  fourierdlem71  46175  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  etransclem48  46280  salgensscntex  46342  sge0tsms  46378  nnfoctbdjlem  46453  isomenndlem  46528  ovnval  46539  ovncvrrp  46562  ovnsubaddlem1  46568  hsphoif  46574  hsphoival  46577  ovnhoilem2  46600  hoidifhspval  46606  ovncvr2  46609  hspmbllem2  46625  vonioolem1  46678  smfpimcclem  46805  smflimsuplem1  46818  smflimsuplem4  46821  smflimsuplem7  46824  smfliminflem  46828  fsupdm  46840  smfsupdmmbllem  46842  finfdm  46844  smfinfdmmbllem  46846  cfsetsnfsetfo  47061  isuspgrim0  47894  cycldlenngric  47928  isgrtri  47942  1aryenef  48634  2aryenef  48645  itcovalpclem2  48660  itcovalt2lem2  48665  ackvalsuc1mpt  48667  ackval0  48669  cofidvala  49105  cofidval  49108  isnatd  49212  swapfelvv  49252  swapf2fvala  49253  swapf1vala  49255  swapf2fn  49257  swapf2vala  49259  tposcurf1  49288  prcofelvv  49369  reldmprcof1  49370  reldmprcof2  49371  prcof1  49377  prcof2a  49378  prcof2  49379  idfudiag1bas  49513  idfudiag1  49514  lmdfval  49638  cmdfval  49639  aacllem  49790