MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mptex Structured version   Visualization version   GIF version

Theorem mptex 6367
Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 6366. (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
StepHypRef Expression
1 mptex.1 . 2 𝐴 ∈ V
2 mptexg 6366 . 2 (𝐴 ∈ V → (𝑥𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝑥𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  Vcvv 3172  cmpt 4637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pr 4827
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4942  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797
This theorem is referenced by:  mptrabex  6369  mptrabexOLD  6370  eufnfv  6372  fvresex  7009  abrexex  7010  ofmres  7032  noinfep  8417  cantnffval  8420  cnfcomlem  8456  cnfcom3clem  8462  fseqenlem1  8707  dfacacn  8823  dfac12lem1  8825  infmap2  8900  ackbij2lem2  8922  ackbij2lem3  8923  fin23lem32  9026  konigthlem  9246  wunex2  9416  wuncval2  9425  rpnnen1lem1  11649  rpnnen1lem3  11650  rpnnen1lem5  11652  rpnnen1lem1OLD  11655  rpnnen1lem3OLD  11656  rpnnen1lem5OLD  11658  mptnn0fsupp  12616  ccatfn  13158  ccatfval  13159  swrdval  13217  swrd00  13218  swrd0  13234  revval  13308  repsundef  13317  climmpt  14098  climle  14166  iserabs  14336  isumshft  14358  divcnvshft  14374  supcvg  14375  trireciplem  14381  expcnv  14383  explecnv  14384  geolim  14388  geo2lim  14393  cvgrat  14402  mertenslem2  14404  eftlub  14626  rpnnen2lem1  14730  rpnnen2lem2  14731  1arithlem1  15413  1arith  15417  vdwapval  15463  vdwlem6  15476  vdwlem9  15479  restfn  15856  cidfval  16108  cidffn  16110  idfu2nd  16308  idfu1st  16310  idfucl  16312  fucco  16393  homafval  16450  idafval  16478  prf1  16611  prf2fval  16612  prfcl  16614  prf1st  16615  prf2nd  16616  curf1fval  16635  curf11  16637  curf12  16638  curf1cl  16639  curf2  16640  curfcl  16643  hof2val  16667  yonedalem3a  16685  yonedalem4a  16686  yonedalem4b  16687  yonedalem4c  16688  yonedalem3  16691  yonedainv  16692  lubfval  16749  glbfval  16762  grpinvfval  17231  grplactfval  17287  cntzfval  17524  psgnfval  17691  odfval  17723  sylow1lem2  17785  sylow2blem1  17806  sylow2blem2  17807  sylow3lem1  17813  sylow3lem6  17818  pj1fval  17878  vrgpfval  17950  lspfval  18742  sraval  18945  aspval  19097  asclfval  19103  psrmulfval  19154  psrass1  19174  mvrval  19190  mplmon  19232  mplcoe1  19234  evlslem2  19281  mpfrcl  19287  evlsval  19288  evlsvar  19292  mpfind  19305  coe1fval  19344  psropprmul  19377  coe1mul2  19408  ply1coe  19435  evls1fval  19453  evls1val  19454  evl1fval  19461  evl1val  19462  zrhval2  19623  submafval  20151  mdetfval  20158  madufval  20209  minmar1fval  20218  pmatcollpw2lem  20348  pm2mpval  20366  1stcfb  21005  ptbasfi  21141  dfac14  21178  fmval  21504  fmf  21506  flffval  21550  fcfval  21594  cnextval  21622  met1stc  22083  pcoval  22566  iscmet3lem3  22840  mbflimsup  23183  mbflim  23185  itg1climres  23231  mbfi1fseqlem2  23233  mbfi1fseqlem4  23235  mbfi1fseqlem6  23237  mbfi1flimlem  23239  mbfmullem2  23241  itg2monolem1  23267  itg2addlem  23275  itg2cnlem1  23278  cpnfval  23445  mdegfval  23570  ig1pval  23680  elply  23699  plyeq0lem  23714  plypf1  23716  geolim3  23842  ulmuni  23894  ulmcau  23897  ulmdvlem1  23902  ulmdvlem3  23904  mbfulm  23908  itgulm  23910  pserval  23912  dvradcnv  23923  pserdvlem2  23930  abelthlem1  23933  abelthlem3  23935  abelthlem6  23938  logtayl  24150  leibpi  24413  dfef2  24441  emcllem4  24469  emcllem6  24471  emcllem7  24472  lgamgulmlem5  24503  lgamgulmlem6  24504  lgamcvg2  24525  basellem6  24556  sqff1o  24652  dchrptlem2  24734  dchrptlem3  24735  2lgslem1  24863  dchrisumlem3  24924  padicfval  25049  padicabvf  25064  istrkg2ld  25103  ishlg  25242  mirval  25295  ishpg  25396  lmif  25422  islmib  25424  axlowdim  25586  wwlkn  26003  clwwlkn  26088  clwwlknprop  26093  eupatrl  26288  numclwlk1lem2  26417  nmoofval  26794  htthlem  26951  pjhfval  27432  pjmfn  27751  hosmval  27771  hommval  27772  hodmval  27773  hfsmval  27774  hfmmval  27775  eigvalfval  27933  brafval  27979  kbfval  27988  rnbra  28143  bra11  28144  padct  28678  fpwrelmap  28689  sgnsv  28851  locfinreflem  29028  ordtconlem1  29091  xrhval  29183  sigapildsys  29345  sxbrsigalem2  29468  eulerpart  29564  dstfrvclim1  29659  ballotlemfval  29671  ballotlemsval  29690  signstfv  29759  cvmliftlem5  30318  mvrsval  30449  mrsubffval  30451  mrsubfval  30452  msubffval  30467  msubfval  30468  msubrn  30473  msubco  30475  mvhfval  30477  msrfval  30481  msubvrs  30504  circum  30615  divcnvlin  30664  climlec3  30665  faclimlem2  30676  faclim2  30680  knoppcnlem1  31446  knoppcnlem6  31451  knoppcnlem7  31452  cnndvlem2  31492  ptrest  32361  poimirlem17  32379  poimirlem20  32382  voliunnfl  32406  volsupnfl  32407  upixp  32477  sdclem2  32491  fdc  32494  lmclim2  32507  geomcau  32508  rrncmslem  32584  lkrfval  33175  pmapfval  33843  pclfvalN  33976  polfvalN  33991  watfvalN  34079  ldilfset  34195  ltrnfset  34204  dilfsetN  34240  trnfsetN  34243  trlfset  34248  trlset  34249  tgrpfset  34833  tendofset  34847  tendopl  34865  tendoi  34883  erngfset  34888  erngfset-rN  34896  dvafset  35093  diaffval  35120  dvhfset  35170  docaffvalN  35211  docafvalN  35212  djaffvalN  35223  dibffval  35230  dibfval  35231  dibopelvalN  35233  dibopelval2  35235  dibelval3  35237  dibn0  35243  dib0  35254  diblsmopel  35261  dicffval  35264  dicn0  35282  dihffval  35320  dihfval  35321  dihopelvalcpre  35338  dihatlat  35424  dihpN  35426  dochffval  35439  dochfval  35440  djhffval  35486  lcfrlem8  35639  lcfrlem9  35640  lcdfval  35678  mapdffval  35716  mapdfval  35717  hvmapffval  35848  hvmapfval  35849  hvmapval  35850  hdmap1ffval  35886  hdmap1fval  35887  hdmapffval  35919  hdmapfval  35920  hgmapffval  35978  hgmapfval  35979  hlhilset  36027  mzpincl  36098  dfac11  36433  dfac21  36437  hbtlem1  36495  hbtlem7  36497  rgspnval  36540  fsovd  37105  dvgrat  37316  radcnvrat  37318  hashnzfzclim  37326  uzmptshftfval  37350  dvradcnv2  37351  binomcxplemrat  37354  binomcxplemcvg  37358  binomcxplemdvsum  37359  binomcxplemnotnn0  37360  addrval  37474  subrval  37475  mulvval  37476  fmuldfeqlem1  38432  fmuldfeq  38433  clim1fr1  38451  climexp  38455  climneg  38460  climdivf  38462  divcnvg  38477  expfac  38507  climresmpt  38509  climsubmpt  38510  dvsinax  38584  dvcosax  38599  ioodvbdlimc1lem2  38605  ioodvbdlimc2lem  38607  dvnprodlem1  38619  dvnprodlem2  38620  dvnprodlem3  38621  stoweidlem59  38735  wallispilem5  38745  wallispi  38746  stirlinglem1  38750  stirlinglem8  38757  stirlinglem14  38763  stirlinglem15  38764  dirkerval  38767  fourierdlem71  38853  fourierdlem103  38885  fourierdlem104  38886  fourierdlem112  38894  etransclem48  38958  salgensscntex  39021  sge0tsms  39056  nnfoctbdjlem  39131  isomenndlem  39203  ovnval  39214  ovncvrrp  39237  ovnsubaddlem1  39243  hsphoif  39249  hsphoival  39252  ovnhoilem2  39275  hoidifhspval  39281  ovncvr2  39284  hspmbllem2  39300  vonioolem1  39354  crctcshlem3  41003  1wlkisowwlkupgr  41058  av-numclwlk1lem2  41508  irinitoringc  41842  aacllem  42298
  Copyright terms: Public domain W3C validator