Theorem mptex 7220

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

Syntax hints:   ∈ wcel 2109  Vcvv 3464   ↦ cmpt 5206

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 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544

This theorem is referenced by:  mptrabex  7222  mptfvmpt  7225  eufnfv  7226  fvresex  7963  ofmres  7988  noinfep  9679  cantnffval  9682  cnfcomlem  9718  cnfcom3clem  9724  ssttrcl  9734  ttrcltr  9735  ttrclselem2  9745  fseqenlem1  10043  dfacacn  10161  dfac12lem1  10163  infmap2  10236  ackbij2lem2  10258  ackbij2lem3  10259  fin23lem32  10363  konigthlem  10587  wunex2  10757  wuncval2  10766  rpnnen1lem1  12999  rpnnen1lem3  13000  rpnnen1lem5  13002  mptnn0fsupp  14020  ccatfn  14595  ccatfval  14596  swrdval  14666  swrd00  14667  swrd0  14681  revval  14783  repsundef  14794  climmpt  15592  climle  15661  iserabs  15836  isumshft  15860  divcnvshft  15876  supcvg  15877  trireciplem  15883  expcnv  15885  explecnv  15886  geolim  15891  geo2lim  15896  cvgrat  15904  mertenslem2  15906  eftlub  16132  rpnnen2lem1  16237  rpnnen2lem2  16238  1arithlem1  16948  1arith  16952  vdwapval  16998  vdwlem6  17011  vdwlem9  17014  restfn  17443  cidffn  17695  idfu2nd  17895  idfu1st  17897  idfucl  17899  fucco  17983  homafval  18047  prf1  18217  prf2fval  18218  prfcl  18220  prf1st  18221  prf2nd  18222  curf1fval  18241  curf11  18243  curf12  18244  curf1cl  18245  curf2  18246  curfcl  18249  hof2val  18273  yonedalem3a  18291  yonedalem4a  18292  yonedalem4b  18293  yonedalem4c  18294  yonedalem3  18297  yonedainv  18298  lubfval  18365  glbfval  18378  smndex1gbas  18885  smndex1gid  18886  smndex1igid  18887  smndex1mnd  18893  smndex1id  18894  smndex1n0mnd  18895  smndex2dbas  18897  smndex2hbas  18899  cntzfval  19308  psgnfval  19486  sylow1lem2  19585  sylow2blem1  19606  sylow2blem2  19607  sylow3lem1  19613  sylow3lem6  19618  pj1fval  19680  vrgpfval  19752  rgspnval  20577  lspfval  20935  sraval  21138  irinitoringc  21445  zrhval2  21474  aspval  21838  psrmulfval  21908  psrass1  21929  mvrval  21947  mplmon  21998  mplcoe1  22000  evlslem2  22042  mpfrcl  22048  evlsval  22049  evlsvar  22053  mpfind  22070  mhpfval  22081  psdval  22102  psdmul  22109  coe1fval  22146  psropprmul  22178  coe1mul2  22211  ply1coe  22241  evls1fval  22262  evls1val  22263  evl1fval  22271  evl1val  22272  submafval  22522  mdetfval  22529  madufval  22580  minmar1fval  22589  pmatcollpw2lem  22720  pm2mpval  22738  1stcfb  23388  ptbasfi  23524  dfac14  23561  fmval  23886  fmf  23888  flffval  23932  fcfval  23976  cnextval  24004  met1stc  24465  pcoval  24967  iscmet3lem3  25247  rrxsca  25353  mbflimsup  25624  mbflim  25626  itg1climres  25672  mbfi1fseqlem2  25674  mbfi1fseqlem4  25676  mbfi1fseqlem6  25678  mbfi1flimlem  25680  mbfmullem2  25682  itg2monolem1  25708  itg2addlem  25716  itg2cnlem1  25719  cpnfval  25891  mdegfval  26024  elply  26157  plyeq0lem  26172  plypf1  26174  geolim3  26304  ulmuni  26358  ulmcau  26361  ulmdvlem1  26366  ulmdvlem3  26368  mbfulm  26372  itgulm  26374  pserval  26376  dvradcnv  26387  pserdvlem2  26395  abelthlem1  26398  abelthlem3  26400  abelthlem6  26403  logtayl  26626  leibpi  26909  dfef2  26938  emcllem4  26966  emcllem6  26968  emcllem7  26969  lgamgulmlem5  27000  lgamgulmlem6  27001  lgamcvg2  27022  basellem6  27053  sqff1o  27149  dchrptlem2  27233  dchrptlem3  27234  2lgslem1  27362  dchrisumlem3  27459  padicfval  27584  padicabvf  27599  istrkg2ld  28444  mirval  28639  ishpg  28743  lmif  28769  islmib  28771  axlowdim  28945  crctcshlem3  29806  nmoofval  30748  pjhfval  31382  pjmfn  31701  hosmval  31721  hommval  31722  hodmval  31723  hfsmval  31724  hfmmval  31725  eigvalfval  31883  brafval  31929  kbfval  31938  rnbra  32093  bra11  32094  padct  32702  fpwrelmap  32715  qusima  33428  nsgmgc  33432  nsgqusf1o  33436  idlsrgtset  33528  locfinreflem  33876  rspectopn  33903  zarcmplem  33917  ordtconnlem1  33960  xrhval  34054  sigapildsys  34198  sxbrsigalem2  34323  eulerpart  34419  dstfrvclim1  34515  ballotlemfval  34527  ballotlemsval  34546  signstfv  34600  vtsval  34674  cvmliftlem5  35316  mrsubffval  35534  mrsubfval  35535  msubffval  35550  msubfval  35551  msubrn  35556  msubco  35558  msubvrs  35587  circum  35701  divcnvlin  35755  climlec3  35756  faclimlem2  35766  faclim2  35770  knoppcnlem1  36516  knoppcnlem6  36521  knoppcnlem7  36522  cnndvlem2  36561  bj-endval  37338  ptrest  37648  poimirlem17  37666  poimirlem20  37669  voliunnfl  37693  volsupnfl  37694  upixp  37758  sdclem2  37771  fdc  37774  lmclim2  37787  geomcau  37788  rrncmslem  37861  pclfvalN  39913  polfvalN  39928  trlset  40185  tendopl  40800  docafvalN  41146  dibfval  41165  dibopelvalN  41167  dibopelval2  41169  dibelval3  41171  dibn0  41177  dib0  41188  diblsmopel  41195  dicn0  41216  dihopelvalcpre  41272  dihatlat  41358  dihpN  41360  dochfval  41374  lcfrlem9  41574  hvmapfval  41783  hvmapval  41784  hdmap1fval  41820  hlhilset  41958  sticksstones10  42173  sticksstones12a  42175  aks6d1c6isolem2  42193  evlsvvvallem2  42560  evlsvvval  42561  selvvvval  42583  evlselv  42585  prjcrvfval  42629  mzpincl  42732  dfac11  43061  dfac21  43065  hbtlem1  43122  hbtlem7  43124  fsovd  44007  mnringmulrcld  44227  dvgrat  44311  radcnvrat  44313  hashnzfzclim  44321  uzmptshftfval  44345  dvradcnv2  44346  binomcxplemrat  44349  binomcxplemcvg  44353  binomcxplemdvsum  44354  binomcxplemnotnn0  44355  addrval  44465  subrval  44466  mulvval  44467  fmuldfeqlem1  45591  fmuldfeq  45592  clim1fr1  45610  climexp  45614  climneg  45619  climdivf  45621  divcnvg  45636  expfac  45666  climresmpt  45668  climsubmpt  45669  limsupval4  45803  climliminflimsupd  45810  liminfreuzlem  45811  liminfltlem  45813  liminfpnfuz  45825  dvsinax  45922  dvcosax  45935  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  dvnprodlem1  45955  dvnprodlem2  45956  dvnprodlem3  45957  stoweidlem59  46068  wallispilem5  46078  wallispi  46079  stirlinglem1  46083  stirlinglem8  46090  stirlinglem14  46096  stirlinglem15  46097  dirkerval  46100  fourierdlem71  46186  fourierdlem103  46218  fourierdlem104  46219  fourierdlem112  46227  etransclem48  46291  salgensscntex  46353  sge0tsms  46389  nnfoctbdjlem  46464  isomenndlem  46539  ovnval  46550  ovncvrrp  46573  ovnsubaddlem1  46579  hsphoif  46585  hsphoival  46588  ovnhoilem2  46611  hoidifhspval  46617  ovncvr2  46620  hspmbllem2  46636  vonioolem1  46689  smfpimcclem  46816  smflimsuplem1  46829  smflimsuplem4  46832  smflimsuplem7  46835  smfliminflem  46839  fsupdm  46851  smfsupdmmbllem  46853  finfdm  46855  smfinfdmmbllem  46857  cfsetsnfsetfo  47069  isuspgrim0  47887  cycldlenngric  47921  isgrtri  47935  1aryenef  48605  2aryenef  48616  itcovalpclem2  48631  itcovalt2lem2  48636  ackvalsuc1mpt  48638  ackval0  48640  isnatd  49123  swapfelvv  49160  swapf2fvala  49161  swapf1vala  49163  swapf2fn  49165  swapf2vala  49167  tposcurf1  49190  prcofelvv  49270  reldmprcof1  49271  reldmprcof2  49272  prcof1  49278  prcof2a  49279  prcof2  49280  idfudiag1bas  49389  idfudiag1  49390  lmdfval  49503  cmdfval  49504  aacllem  49645