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

Theorem mptex 7174
Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7172. (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 7172 . 2 (𝐴 ∈ V → (𝑥𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝑥𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3444  cmpt 5189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505
This theorem is referenced by:  mptrabex  7176  mptfvmpt  7179  eufnfv  7180  fvresex  7893  ofmres  7918  noinfep  9601  cantnffval  9604  cnfcomlem  9640  cnfcom3clem  9646  ssttrcl  9656  ttrcltr  9657  ttrclselem2  9667  fseqenlem1  9965  dfacacn  10082  dfac12lem1  10084  infmap2  10159  ackbij2lem2  10181  ackbij2lem3  10182  fin23lem32  10285  konigthlem  10509  wunex2  10679  wuncval2  10688  rpnnen1lem1  12908  rpnnen1lem3  12909  rpnnen1lem5  12911  mptnn0fsupp  13908  ccatfn  14466  ccatfval  14467  swrdval  14537  swrd00  14538  swrd0  14552  revval  14654  repsundef  14665  climmpt  15459  climle  15528  iserabs  15705  isumshft  15729  divcnvshft  15745  supcvg  15746  trireciplem  15752  expcnv  15754  explecnv  15755  geolim  15760  geo2lim  15765  cvgrat  15773  mertenslem2  15775  eftlub  15996  rpnnen2lem1  16101  rpnnen2lem2  16102  1arithlem1  16800  1arith  16804  vdwapval  16850  vdwlem6  16863  vdwlem9  16866  restfn  17311  cidffn  17563  idfu2nd  17768  idfu1st  17770  idfucl  17772  fucco  17856  homafval  17920  prf1  18093  prf2fval  18094  prfcl  18096  prf1st  18097  prf2nd  18098  curf1fval  18118  curf11  18120  curf12  18121  curf1cl  18122  curf2  18123  curfcl  18126  hof2val  18150  yonedalem3a  18168  yonedalem4a  18169  yonedalem4b  18170  yonedalem4c  18171  yonedalem3  18174  yonedainv  18175  lubfval  18244  glbfval  18257  smndex1gbas  18717  smndex1gid  18718  smndex1igid  18719  smndex1mnd  18725  smndex1id  18726  smndex1n0mnd  18727  smndex2dbas  18729  smndex2hbas  18731  cntzfval  19105  psgnfval  19287  sylow1lem2  19386  sylow2blem1  19407  sylow2blem2  19408  sylow3lem1  19414  sylow3lem6  19419  pj1fval  19481  vrgpfval  19553  lspfval  20449  sraval  20653  zrhval2  20925  aspval  21292  psrmulfval  21369  psrass1  21390  mvrval  21406  mplmon  21452  mplcoe1  21454  evlslem2  21505  mpfrcl  21511  evlsval  21512  evlsvar  21516  mpfind  21533  mhpfval  21545  coe1fval  21592  psropprmul  21625  coe1mul2  21656  ply1coe  21683  evls1fval  21701  evls1val  21702  evl1fval  21710  evl1val  21711  submafval  21944  mdetfval  21951  madufval  22002  minmar1fval  22011  pmatcollpw2lem  22142  pm2mpval  22160  1stcfb  22812  ptbasfi  22948  dfac14  22985  fmval  23310  fmf  23312  flffval  23356  fcfval  23400  cnextval  23428  met1stc  23893  pcoval  24390  iscmet3lem3  24670  rrxsca  24776  mbflimsup  25046  mbflim  25048  itg1climres  25095  mbfi1fseqlem2  25097  mbfi1fseqlem4  25099  mbfi1fseqlem6  25101  mbfi1flimlem  25103  mbfmullem2  25105  itg2monolem1  25131  itg2addlem  25139  itg2cnlem1  25142  cpnfval  25312  mdegfval  25443  elply  25572  plyeq0lem  25587  plypf1  25589  geolim3  25715  ulmuni  25767  ulmcau  25770  ulmdvlem1  25775  ulmdvlem3  25777  mbfulm  25781  itgulm  25783  pserval  25785  dvradcnv  25796  pserdvlem2  25803  abelthlem1  25806  abelthlem3  25808  abelthlem6  25811  logtayl  26031  leibpi  26308  dfef2  26336  emcllem4  26364  emcllem6  26366  emcllem7  26367  lgamgulmlem5  26398  lgamgulmlem6  26399  lgamcvg2  26420  basellem6  26451  sqff1o  26547  dchrptlem2  26629  dchrptlem3  26630  2lgslem1  26758  dchrisumlem3  26855  padicfval  26980  padicabvf  26995  istrkg2ld  27444  mirval  27639  ishpg  27743  lmif  27769  islmib  27771  axlowdim  27952  crctcshlem3  28806  nmoofval  29746  pjhfval  30380  pjmfn  30699  hosmval  30719  hommval  30720  hodmval  30721  hfsmval  30722  hfmmval  30723  eigvalfval  30881  brafval  30927  kbfval  30936  rnbra  31091  bra11  31092  padct  31683  fpwrelmap  31697  qusima  32235  nsgmgc  32238  nsgqusf1o  32242  idlsrgtset  32298  locfinreflem  32478  rspectopn  32505  zarcmplem  32519  ordtconnlem1  32562  xrhval  32656  sigapildsys  32818  sxbrsigalem2  32943  eulerpart  33039  dstfrvclim1  33134  ballotlemfval  33146  ballotlemsval  33165  signstfv  33232  vtsval  33307  cvmliftlem5  33940  mrsubffval  34158  mrsubfval  34159  msubffval  34174  msubfval  34175  msubrn  34180  msubco  34182  msubvrs  34211  circum  34319  divcnvlin  34361  climlec3  34362  faclimlem2  34373  faclim2  34377  knoppcnlem1  35002  knoppcnlem6  35007  knoppcnlem7  35008  cnndvlem2  35047  bj-endval  35832  ptrest  36123  poimirlem17  36141  poimirlem20  36144  voliunnfl  36168  volsupnfl  36169  upixp  36234  sdclem2  36247  fdc  36250  lmclim2  36263  geomcau  36264  rrncmslem  36337  pclfvalN  38398  polfvalN  38413  trlset  38670  tendopl  39285  docafvalN  39631  dibfval  39650  dibopelvalN  39652  dibopelval2  39654  dibelval3  39656  dibn0  39662  dib0  39673  diblsmopel  39680  dicn0  39701  dihopelvalcpre  39757  dihatlat  39843  dihpN  39845  dochfval  39859  lcfrlem9  40059  hvmapfval  40268  hvmapval  40269  hdmap1fval  40305  hlhilset  40443  sticksstones10  40609  sticksstones12a  40611  evlsbagval  40791  mhphf  40814  prjcrvfval  41012  mzpincl  41100  dfac11  41432  dfac21  41436  hbtlem1  41493  hbtlem7  41495  rgspnval  41538  fsovd  42368  mnringmulrcld  42596  dvgrat  42680  radcnvrat  42682  hashnzfzclim  42690  uzmptshftfval  42714  dvradcnv2  42715  binomcxplemrat  42718  binomcxplemcvg  42722  binomcxplemdvsum  42723  binomcxplemnotnn0  42724  addrval  42834  subrval  42835  mulvval  42836  fmuldfeqlem1  43909  fmuldfeq  43910  clim1fr1  43928  climexp  43932  climneg  43937  climdivf  43939  divcnvg  43954  expfac  43984  climresmpt  43986  climsubmpt  43987  limsupval4  44121  climliminflimsupd  44128  liminfreuzlem  44129  liminfltlem  44131  liminfpnfuz  44143  dvsinax  44240  dvcosax  44253  ioodvbdlimc1lem2  44259  ioodvbdlimc2lem  44261  dvnprodlem1  44273  dvnprodlem2  44274  dvnprodlem3  44275  stoweidlem59  44386  wallispilem5  44396  wallispi  44397  stirlinglem1  44401  stirlinglem8  44408  stirlinglem14  44414  stirlinglem15  44415  dirkerval  44418  fourierdlem71  44504  fourierdlem103  44536  fourierdlem104  44537  fourierdlem112  44545  etransclem48  44609  salgensscntex  44671  sge0tsms  44707  nnfoctbdjlem  44782  isomenndlem  44857  ovnval  44868  ovncvrrp  44891  ovnsubaddlem1  44897  hsphoif  44903  hsphoival  44906  ovnhoilem2  44929  hoidifhspval  44935  ovncvr2  44938  hspmbllem2  44954  vonioolem1  45007  smfpimcclem  45134  smflimsuplem1  45147  smflimsuplem4  45150  smflimsuplem7  45153  smfliminflem  45157  fsupdm  45169  smfsupdmmbllem  45171  finfdm  45173  smfinfdmmbllem  45175  cfsetsnfsetfo  45380  isomuspgrlem2  46111  irinitoringc  46453  1aryenef  46817  2aryenef  46828  itcovalpclem2  46843  itcovalt2lem2  46848  ackvalsuc1mpt  46850  ackval0  46852  aacllem  47334
  Copyright terms: Public domain W3C validator