Theorem mptex 7252

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   ↦ cmpt 5189

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566

This theorem is used by:  mptrabex  7254  mptfvmpt  7257  eufnfv  7258  fvresex  7996  ofmres  8020  noinfep  9688  cantnffval  9691  cnfcomlem  9727  cnfcom3clem  9733  ssttrcl  9743  ttrcltr  9744  ttrclselem2  9754  fseqenlem1  10130  dfacacn  10247  dfac12lem1  10249  infmap2  10322  ackbij2lem2  10344  ackbij2lem3  10345  fin23lem32  10449  konigthlem  10680  wunex2  10850  wuncval2  10859  rpnnen1lem1  13133  rpnnen1lem3  13134  rpnnen1lem5  13136  mptnn0fsupp  14167  ccatfn  14744  ccatfval  14745  swrdval  14819  swrd00  14820  swrd0  14836  revval  14937  repsundef  14950  climmpt  15767  climle  15836  iserabs  16011  isumshft  16037  divcnvshft  16053  supcvg  16054  trireciplem  16060  expcnv  16062  explecnv  16063  geolim  16068  geo2lim  16073  cvgrat  16081  mertenslem2  16083  eftlub  16306  rpnnen2lem1  16411  rpnnen2lem2  16412  1arithlem1  17130  1arith  17134  vdwapval  17180  vdwlem6  17193  vdwlem9  17196  restfn  17624  cidffn  17881  idfu2nd  18081  idfu1st  18083  idfucl  18085  fucco  18169  homafval  18233  prf1  18403  prf2fval  18404  prfcl  18406  prf1st  18407  prf2nd  18408  curf1fval  18427  curf11  18429  curf12  18430  curf1cl  18431  curf2  18432  curfcl  18435  hof2val  18459  yonedalem3a  18477  yonedalem4a  18478  yonedalem4b  18479  yonedalem4c  18480  yonedalem3  18483  yonedainv  18484  lubfval  18551  glbfval  18564  smndex1gbasOLD  19128  smndex1gidOLD  19130  smndex1igidOLD  19132  smndex1mnd  19138  smndex1id  19139  smndex1n0mnd  19140  smndex2dbas  19142  smndex2hbas  19144  cntzfval  19564  psgnfval  19744  sylow1lem2  19843  sylow2blem1  19864  sylow2blem2  19865  sylow3lem1  19871  sylow3lem6  19876  pj1fval  19938  vrgpfval  20010  rgspnval  20894  lspfval  21278  sraval  21480  irinitoringc  21815  zrhval2  21844  aspval  22210  psrmulfval  22281  psrass1  22301  mvrval  22319  mplmon  22374  mplcoe1  22376  evlslem2  22418  mpfrcl  22424  evlsval  22425  evlsvvvallem2  22431  evlsvvval  22432  evlsvar  22434  mpfind  22454  selvvvval  22481  mhpfval  22489  psdval  22510  psdmul  22517  coe1fval  22553  psropprmul  22585  coe1mul2  22618  ply1coe  22646  evls1fval  22667  evls1val  22668  evl1fval  22676  evl1val  22677  submafval  22924  mdetfval  22931  madufval  22982  minmar1fval  22991  pmatcollpw2lem  23125  pm2mpval  23143  1stcfb  23793  ptbasfi  23930  dfac14  23967  fmval  24292  fmf  24294  flffval  24338  fcfval  24382  cnextval  24410  met1stc  24870  pcoval  25362  iscmet3lem3  25641  rrxsca  25747  mbflimsup  26017  mbflim  26019  itg1climres  26065  mbfi1fseqlem2  26067  mbfi1fseqlem4  26069  mbfi1fseqlem6  26071  mbfi1flimlem  26073  mbfmullem2  26075  itg2monolem1  26101  itg2addlem  26109  itg2cnlem1  26112  cpnfval  26282  mdegfval  26410  elply  26543  plyeq0lem  26559  plypf1  26561  geolim3  26696  ulmuni  26749  ulmcau  26752  ulmdvlem1  26757  ulmdvlem3  26759  mbfulm  26763  itgulm  26765  pserval  26767  dvradcnv  26778  pserdvlem2  26785  abelthlem1  26788  abelthlem3  26790  abelthlem6  26793  logtayl  27018  leibpi  27300  dfef2  27328  emcllem4  27356  emcllem6  27358  emcllem7  27359  lgamgulmlem5  27390  lgamgulmlem6  27391  lgamcvg2  27412  basellem6  27443  sqff1o  27539  dchrptlem2  27622  dchrptlem3  27623  2lgslem1  27751  dchrisumlem3  27848  padicfval  27973  padicabvf  27988  mirval  29157  ishpg  29267  lmif  29320  islmib  29322  axlowdim  29569  crctcshlem3  30438  nmoofval  31394  pjhfval  32028  pjmfn  32347  hosmval  32367  hommval  32368  hodmval  32369  hfsmval  32370  hfmmval  32371  eigvalfval  32529  brafval  32575  kbfval  32584  rnbra  32739  bra11  32740  fpwrelmap  33395  qusima  34029  nsgmgc  34033  nsgqusf1o  34037  idlsrgtset  34110  extvfval  34234  mplvrpmga  34247  esplyval  34264  locfinreflem  34542  rspectopn  34569  zarcmplem  34583  ordtconnlem1  34626  xrhval  34720  sigapildsys  34865  sxbrsigalem2  34988  eulerpart  35084  dstfrvclim1  35180  ballotlemfval  35192  ballotlemsval  35211  signstfv  35262  vtsval  35336  fineqvnttrclse  35892  cvmliftlem5  36221  mrsubffval  36439  mrsubfval  36440  msubffval  36455  msubfval  36456  msubrn  36461  msubco  36463  msubvrs  36492  circum  36606  mirimanoffr  36627  divcnvlin  36676  climlec3  36677  faclimlem2  36687  faclim2  36691  knoppcnlem1  37537  knoppcnlem6  37542  knoppcnlem7  37543  cnndvlem2  37582  bj-endval  38428  ptrest  38729  poimirlem17  38747  poimirlem20  38750  voliunnfl  38774  volsupnfl  38775  upixp  38855  sdclem2  38868  fdc  38871  lmclim2  38884  geomcau  38885  rrncmslem  38958  pclfvalN  41138  polfvalN  41153  trlset  41410  tendopl  42025  docafvalN  42371  dibfval  42390  dibopelvalN  42392  dibopelval2  42394  dibelval3  42396  dibn0  42402  dib0  42413  diblsmopel  42420  dicn0  42441  dihopelvalcpre  42497  dihatlat  42583  dihpN  42585  dochfval  42599  lcfrlem9  42799  hvmapfval  43008  hvmapval  43009  hdmap1fval  43045  hlhilset  43183  sticksstones10  43397  sticksstones12a  43399  aks6d1c6isolem2  43417  evlselv  43810  prjcrvfval  43860  mzpincl  43938  dfac11  44257  dfac21  44261  hbtlem1  44317  hbtlem7  44319  fsovd  45200  mnringmulrcld  45418  dvgrat  45488  radcnvrat  45490  hashnzfzclim  45498  uzmptshftfval  45522  dvradcnv2  45523  binomcxplemrat  45526  binomcxplemcvg  45530  binomcxplemdvsum  45531  binomcxplemnotnn0  45532  addrval  45639  subrval  45640  mulvval  45641  fmuldfeqlem1  46799  fmuldfeq  46800  clim1fr1  46818  climexp  46822  climneg  46827  climdivf  46829  divcnvg  46844  expfac  46872  climresmpt  46874  climsubmpt  46875  limsupval4  47009  climliminflimsupd  47016  liminfreuzlem  47017  liminfltlem  47019  liminfpnfuz  47031  dvsinax  47128  dvcosax  47141  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  dvnprodlem1  47161  dvnprodlem2  47162  dvnprodlem3  47163  stoweidlem59  47274  wallispilem5  47284  wallispi  47285  stirlinglem1  47289  stirlinglem8  47296  stirlinglem14  47302  stirlinglem15  47303  dirkerval  47306  fourierdlem71  47392  fourierdlem103  47424  fourierdlem104  47425  fourierdlem112  47433  etransclem48  47497  salgensscntex  47559  sge0tsms  47595  nnfoctbdjlem  47670  isomenndlem  47745  ovnval  47756  ovncvrrp  47779  ovnsubaddlem1  47785  hsphoif  47791  hsphoival  47794  ovnhoilem2  47817  hoidifhspval  47823  ovncvr2  47826  hspmbllem2  47842  vonioolem1  47895  smfpimcclem  48022  smflimsuplem1  48035  smflimsuplem4  48038  smflimsuplem7  48041  smfliminflem  48045  fsupdm  48057  smfsupdmmbllem  48059  finfdm  48061  smfinfdmmbllem  48063  cfsetsnfsetfo  48335  isuspgrim0  49197  cycldlenngric  49231  isgrtri  49246  1aryenef  49962  2aryenef  49973  itcovalpclem2  49988  itcovalt2lem2  49993  ackvalsuc1mpt  49995  ackval0  49997  fnmpompt  50186  ovmpomptd  50187  cofidvala  50437  cofidval  50440  isnatd  50544  swapfelvv  50590  swapf2fvala  50591  swapf1vala  50593  swapf2fn  50595  swapf2vala  50597  tposcurf1  50626  postcof1st  50703  postcof2nd  50704  postcof2  50705  prcofelvv  50720  reldmprcof1  50721  reldmprcof2  50722  prcof1  50728  prcof2a  50729  prcof2  50730  idfudiag1bas  50864  idfudiag1  50865  fuconuniqlem  50986  fuconuniqvalslem  50988  lmdfval  51037  cmdfval  51038  aacllem  51219  crosspval  51234  veronesevald  51251