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

Theorem mptex 6721
Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 6719. (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 6719 . 2 (𝐴 ∈ V → (𝑥𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝑥𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2157  Vcvv 3402  cmpt 4934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pr 5109
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5232  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119
This theorem is referenced by:  mptrabex  6723  mptfvmpt  6725  eufnfv  6726  fvresex  7379  abrexexOLD  7382  ofmres  7404  noinfep  8814  cantnffval  8817  cnfcomlem  8853  cnfcom3clem  8859  fseqenlem1  9140  dfacacn  9258  dfac12lem1  9260  infmap2  9335  ackbij2lem2  9357  ackbij2lem3  9358  fin23lem32  9461  konigthlem  9685  wunex2  9855  wuncval2  9864  rpnnen1lem1  12054  rpnnen1lem3  12055  rpnnen1lem5  12057  mptnn0fsupp  13040  ccatfn  13589  ccatfval  13590  swrdval  13660  swrd00  13661  swrd0  13678  revval  13753  repsundef  13762  climmpt  14545  climle  14613  iserabs  14789  isumshft  14813  divcnvshft  14829  supcvg  14830  trireciplem  14836  expcnv  14838  explecnv  14839  geolim  14843  geo2lim  14848  cvgrat  14856  mertenslem2  14858  eftlub  15079  rpnnen2lem1  15183  rpnnen2lem2  15184  1arithlem1  15864  1arith  15868  vdwapval  15914  vdwlem6  15927  vdwlem9  15930  restfn  16310  cidffn  16563  idfu2nd  16761  idfu1st  16763  idfucl  16765  fucco  16846  homafval  16903  prf1  17065  prf2fval  17066  prfcl  17068  prf1st  17069  prf2nd  17070  curf1fval  17089  curf11  17091  curf12  17092  curf1cl  17093  curf2  17094  curfcl  17097  hof2val  17121  yonedalem3a  17139  yonedalem4a  17140  yonedalem4b  17141  yonedalem4c  17142  yonedalem3  17145  yonedainv  17146  lubfval  17203  glbfval  17216  cntzfval  17974  psgnfval  18141  sylow1lem2  18235  sylow2blem1  18256  sylow2blem2  18257  sylow3lem1  18263  sylow3lem6  18268  pj1fval  18328  vrgpfval  18400  lspfval  19200  sraval  19405  aspval  19557  psrmulfval  19614  psrass1  19634  mvrval  19650  mplmon  19692  mplcoe1  19694  evlslem2  19740  mpfrcl  19746  evlsval  19747  evlsvar  19751  mpfind  19764  coe1fval  19803  psropprmul  19836  coe1mul2  19867  ply1coe  19894  evls1fval  19912  evls1val  19913  evl1fval  19920  evl1val  19921  zrhval2  20085  submafval  20617  mdetfval  20624  madufval  20675  minmar1fval  20684  pmatcollpw2lem  20816  pm2mpval  20834  1stcfb  21483  ptbasfi  21619  dfac14  21656  fmval  21981  fmf  21983  flffval  22027  fcfval  22071  cnextval  22099  met1stc  22560  pcoval  23044  iscmet3lem3  23322  mbflimsup  23670  mbflim  23672  itg1climres  23718  mbfi1fseqlem2  23720  mbfi1fseqlem4  23722  mbfi1fseqlem6  23724  mbfi1flimlem  23726  mbfmullem2  23728  itg2monolem1  23754  itg2addlem  23762  itg2cnlem1  23765  cpnfval  23932  mdegfval  24059  elply  24188  plyeq0lem  24203  plypf1  24205  geolim3  24331  ulmuni  24383  ulmcau  24386  ulmdvlem1  24391  ulmdvlem3  24393  mbfulm  24397  itgulm  24399  pserval  24401  dvradcnv  24412  pserdvlem2  24419  abelthlem1  24422  abelthlem3  24424  abelthlem6  24427  logtayl  24643  leibpi  24906  dfef2  24934  emcllem4  24962  emcllem6  24964  emcllem7  24965  lgamgulmlem5  24996  lgamgulmlem6  24997  lgamcvg2  25018  basellem6  25049  sqff1o  25145  dchrptlem2  25227  dchrptlem3  25228  2lgslem1  25356  dchrisumlem3  25417  padicfval  25542  padicabvf  25557  istrkg2ld  25596  mirval  25787  ishpg  25888  lmif  25914  islmib  25916  axlowdim  26078  crctcshlem3  26963  nmoofval  27968  pjhfval  28606  pjmfn  28925  hosmval  28945  hommval  28946  hodmval  28947  hfsmval  28948  hfmmval  28949  eigvalfval  29107  brafval  29153  kbfval  29162  rnbra  29317  bra11  29318  padct  29847  fpwrelmap  29858  locfinreflem  30255  ordtconnlem1  30318  xrhval  30410  sigapildsys  30573  sxbrsigalem2  30696  eulerpart  30792  dstfrvclim1  30887  ballotlemfval  30899  ballotlemsval  30918  signstfv  30988  vtsval  31063  cvmliftlem5  31616  mrsubffval  31749  mrsubfval  31750  msubffval  31765  msubfval  31766  msubrn  31771  msubco  31773  msubvrs  31802  circum  31912  divcnvlin  31962  climlec3  31963  faclimlem2  31974  faclim2  31978  knoppcnlem1  32822  knoppcnlem6  32827  knoppcnlem7  32828  cnndvlem2  32868  ptrest  33740  poimirlem17  33758  poimirlem20  33761  voliunnfl  33785  volsupnfl  33786  upixp  33855  sdclem2  33868  fdc  33871  lmclim2  33884  geomcau  33885  rrncmslem  33961  pclfvalN  35688  polfvalN  35703  trlset  35960  tendopl  36575  docafvalN  36921  dibfval  36940  dibopelvalN  36942  dibopelval2  36944  dibelval3  36946  dibn0  36952  dib0  36963  diblsmopel  36970  dicn0  36991  dihopelvalcpre  37047  dihatlat  37133  dihpN  37135  dochfval  37149  lcfrlem9  37349  hvmapfval  37558  hvmapval  37559  hdmap1fval  37595  hlhilset  37733  mzpincl  37817  dfac11  38151  dfac21  38155  hbtlem1  38212  hbtlem7  38214  rgspnval  38257  fsovd  38820  dvgrat  39029  radcnvrat  39031  hashnzfzclim  39039  uzmptshftfval  39063  dvradcnv2  39064  binomcxplemrat  39067  binomcxplemcvg  39071  binomcxplemdvsum  39072  binomcxplemnotnn0  39073  addrval  39186  subrval  39187  mulvval  39188  fmuldfeqlem1  40312  fmuldfeq  40313  clim1fr1  40331  climexp  40335  climneg  40340  climdivf  40342  divcnvg  40357  expfac  40387  climresmpt  40389  climsubmpt  40390  limsupval4  40524  climliminflimsupd  40531  liminfreuzlem  40532  liminfltlem  40534  dvsinax  40625  dvcosax  40639  ioodvbdlimc1lem2  40645  ioodvbdlimc2lem  40647  dvnprodlem1  40659  dvnprodlem2  40660  dvnprodlem3  40661  stoweidlem59  40773  wallispilem5  40783  wallispi  40784  stirlinglem1  40788  stirlinglem8  40795  stirlinglem14  40801  stirlinglem15  40802  dirkerval  40805  fourierdlem71  40891  fourierdlem103  40923  fourierdlem104  40924  fourierdlem112  40932  etransclem48  40996  salgensscntex  41059  sge0tsms  41094  nnfoctbdjlem  41169  isomenndlem  41244  ovnval  41255  ovncvrrp  41278  ovnsubaddlem1  41284  hsphoif  41290  hsphoival  41293  ovnhoilem2  41316  hoidifhspval  41322  ovncvr2  41325  hspmbllem2  41341  vonioolem1  41394  smfpimcclem  41513  smflimsuplem1  41526  smflimsuplem4  41529  smflimsuplem7  41532  smfliminflem  41536  irinitoringc  42655  aacllem  43136
  Copyright terms: Public domain W3C validator