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

Theorem mptex 6527
Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 6525. (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 6525 . 2 (𝐴 ∈ V → (𝑥𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝑥𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231  cmpt 4762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934
This theorem is referenced by:  mptrabex  6529  eufnfv  6531  fvresex  7181  abrexexOLD  7184  ofmres  7206  noinfep  8595  cantnffval  8598  cnfcomlem  8634  cnfcom3clem  8640  fseqenlem1  8885  dfacacn  9001  dfac12lem1  9003  infmap2  9078  ackbij2lem2  9100  ackbij2lem3  9101  fin23lem32  9204  konigthlem  9428  wunex2  9598  wuncval2  9607  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  mptnn0fsupp  12837  ccatfn  13390  ccatfval  13391  swrdval  13462  swrd00  13463  swrd0  13480  revval  13555  repsundef  13564  climmpt  14346  climle  14414  iserabs  14591  isumshft  14615  divcnvshft  14631  supcvg  14632  trireciplem  14638  expcnv  14640  explecnv  14641  geolim  14645  geo2lim  14650  cvgrat  14659  mertenslem2  14661  eftlub  14883  rpnnen2lem1  14987  rpnnen2lem2  14988  1arithlem1  15674  1arith  15678  vdwapval  15724  vdwlem6  15737  vdwlem9  15740  restfn  16132  cidfval  16384  cidffn  16386  idfu2nd  16584  idfu1st  16586  idfucl  16588  fucco  16669  homafval  16726  idafval  16754  prf1  16887  prf2fval  16888  prfcl  16890  prf1st  16891  prf2nd  16892  curf1fval  16911  curf11  16913  curf12  16914  curf1cl  16915  curf2  16916  curfcl  16919  hof2val  16943  yonedalem3a  16961  yonedalem4a  16962  yonedalem4b  16963  yonedalem4c  16964  yonedalem3  16967  yonedainv  16968  lubfval  17025  glbfval  17038  grpinvfval  17507  grplactfval  17563  cntzfval  17799  psgnfval  17966  odfval  17998  sylow1lem2  18060  sylow2blem1  18081  sylow2blem2  18082  sylow3lem1  18088  sylow3lem6  18093  pj1fval  18153  vrgpfval  18225  lspfval  19021  sraval  19224  aspval  19376  asclfval  19382  psrmulfval  19433  psrass1  19453  mvrval  19469  mplmon  19511  mplcoe1  19513  evlslem2  19560  mpfrcl  19566  evlsval  19567  evlsvar  19571  mpfind  19584  coe1fval  19623  psropprmul  19656  coe1mul2  19687  ply1coe  19714  evls1fval  19732  evls1val  19733  evl1fval  19740  evl1val  19741  zrhval2  19905  submafval  20433  mdetfval  20440  madufval  20491  minmar1fval  20500  pmatcollpw2lem  20630  pm2mpval  20648  1stcfb  21296  ptbasfi  21432  dfac14  21469  fmval  21794  fmf  21796  flffval  21840  fcfval  21884  cnextval  21912  met1stc  22373  pcoval  22857  iscmet3lem3  23134  mbflimsup  23478  mbflim  23480  itg1climres  23526  mbfi1fseqlem2  23528  mbfi1fseqlem4  23530  mbfi1fseqlem6  23532  mbfi1flimlem  23534  mbfmullem2  23536  itg2monolem1  23562  itg2addlem  23570  itg2cnlem1  23573  cpnfval  23740  mdegfval  23867  ig1pval  23977  elply  23996  plyeq0lem  24011  plypf1  24013  geolim3  24139  ulmuni  24191  ulmcau  24194  ulmdvlem1  24199  ulmdvlem3  24201  mbfulm  24205  itgulm  24207  pserval  24209  dvradcnv  24220  pserdvlem2  24227  abelthlem1  24230  abelthlem3  24232  abelthlem6  24235  logtayl  24451  leibpi  24714  dfef2  24742  emcllem4  24770  emcllem6  24772  emcllem7  24773  lgamgulmlem5  24804  lgamgulmlem6  24805  lgamcvg2  24826  basellem6  24857  sqff1o  24953  dchrptlem2  25035  dchrptlem3  25036  2lgslem1  25164  dchrisumlem3  25225  padicfval  25350  padicabvf  25365  istrkg2ld  25404  ishlg  25542  mirval  25595  ishpg  25696  lmif  25722  islmib  25724  axlowdim  25886  crctcshlem3  26767  wlkisowwlkupgr  26834  nmoofval  27745  htthlem  27902  pjhfval  28383  pjmfn  28702  hosmval  28722  hommval  28723  hodmval  28724  hfsmval  28725  hfmmval  28726  eigvalfval  28884  brafval  28930  kbfval  28939  rnbra  29094  bra11  29095  padct  29625  fpwrelmap  29636  sgnsv  29855  locfinreflem  30035  ordtconnlem1  30098  xrhval  30190  sigapildsys  30353  sxbrsigalem2  30476  eulerpart  30572  dstfrvclim1  30667  ballotlemfval  30679  ballotlemsval  30698  signstfv  30768  vtsval  30843  cvmliftlem5  31397  mvrsval  31528  mrsubffval  31530  mrsubfval  31531  msubffval  31546  msubfval  31547  msubrn  31552  msubco  31554  mvhfval  31556  msrfval  31560  msubvrs  31583  circum  31694  divcnvlin  31744  climlec3  31745  faclimlem2  31756  faclim2  31760  knoppcnlem1  32608  knoppcnlem6  32613  knoppcnlem7  32614  cnndvlem2  32654  ptrest  33538  poimirlem17  33556  poimirlem20  33559  voliunnfl  33583  volsupnfl  33584  upixp  33654  sdclem2  33668  fdc  33671  lmclim2  33684  geomcau  33685  rrncmslem  33761  lkrfval  34692  pmapfval  35360  pclfvalN  35493  polfvalN  35508  watfvalN  35596  ldilfset  35712  ltrnfset  35721  dilfsetN  35757  trnfsetN  35760  trlfset  35765  trlset  35766  tgrpfset  36349  tendofset  36363  tendopl  36381  tendoi  36399  erngfset  36404  erngfset-rN  36412  dvafset  36609  diaffval  36636  dvhfset  36686  docaffvalN  36727  docafvalN  36728  djaffvalN  36739  dibffval  36746  dibfval  36747  dibopelvalN  36749  dibopelval2  36751  dibelval3  36753  dibn0  36759  dib0  36770  diblsmopel  36777  dicffval  36780  dicn0  36798  dihffval  36836  dihfval  36837  dihopelvalcpre  36854  dihatlat  36940  dihpN  36942  dochffval  36955  dochfval  36956  djhffval  37002  lcfrlem8  37155  lcfrlem9  37156  lcdfval  37194  mapdffval  37232  mapdfval  37233  hvmapffval  37364  hvmapfval  37365  hvmapval  37366  hdmap1ffval  37402  hdmap1fval  37403  hdmapffval  37435  hdmapfval  37436  hgmapffval  37494  hgmapfval  37495  hlhilset  37543  mzpincl  37614  dfac11  37949  dfac21  37953  hbtlem1  38010  hbtlem7  38012  rgspnval  38055  fsovd  38619  dvgrat  38828  radcnvrat  38830  hashnzfzclim  38838  uzmptshftfval  38862  dvradcnv2  38863  binomcxplemrat  38866  binomcxplemcvg  38870  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  addrval  38987  subrval  38988  mulvval  38989  fmuldfeqlem1  40132  fmuldfeq  40133  clim1fr1  40151  climexp  40155  climneg  40160  climdivf  40162  divcnvg  40177  expfac  40207  climresmpt  40209  climsubmpt  40210  limsupval4  40344  climliminflimsupd  40351  liminfreuzlem  40352  liminfltlem  40354  dvsinax  40445  dvcosax  40459  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  stoweidlem59  40594  wallispilem5  40604  wallispi  40605  stirlinglem1  40609  stirlinglem8  40616  stirlinglem14  40622  stirlinglem15  40623  dirkerval  40626  fourierdlem71  40712  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  etransclem48  40817  salgensscntex  40880  sge0tsms  40915  nnfoctbdjlem  40990  isomenndlem  41065  ovnval  41076  ovncvrrp  41099  ovnsubaddlem1  41105  hsphoif  41111  hsphoival  41114  ovnhoilem2  41137  hoidifhspval  41143  ovncvr2  41146  hspmbllem2  41162  vonioolem1  41215  smfpimcclem  41334  smflimsuplem1  41347  smflimsuplem4  41350  smflimsuplem7  41353  smfliminflem  41357  irinitoringc  42394  aacllem  42875
  Copyright terms: Public domain W3C validator