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

Theorem fvmpt2 6248
Description: Value of a function given by the "maps to" notation. (Contributed by FL, 21-Jun-2010.)
Hypothesis
Ref Expression
mptrcl.1 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
fvmpt2 ((𝑥𝐴𝐵𝐶) → (𝐹𝑥) = 𝐵)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝐹(𝑥)

Proof of Theorem fvmpt2
StepHypRef Expression
1 mptrcl.1 . . 3 𝐹 = (𝑥𝐴𝐵)
21fvmpt2i 6247 . 2 (𝑥𝐴 → (𝐹𝑥) = ( I ‘𝐵))
3 fvi 6212 . 2 (𝐵𝐶 → ( I ‘𝐵) = 𝐵)
42, 3sylan9eq 2675 1 ((𝑥𝐴𝐵𝐶) → (𝐹𝑥) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  cmpt 4673   I cid 4984  cfv 5847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fv 5855
This theorem is referenced by:  fvmptss  6249  fvmpt2d  6250  fvmptdf  6252  mpteqb  6255  fvmptt  6256  fvmptf  6257  fnmptfvd  6276  ralrnmpt  6324  fmptco  6351  f1mpt  6472  offval2  6867  ofrfval2  6868  mptelixpg  7889  dom2lem  7939  mapxpen  8070  xpmapenlem  8071  cnfcom3clem  8546  tcvalg  8558  rankf  8601  infxpenc2lem2  8787  dfac8clem  8799  acni2  8813  acnlem  8815  fin23lem32  9110  axcc2lem  9202  axcc3  9204  domtriomlem  9208  ac6num  9245  konigthlem  9334  rpnnen1lem1  11759  rpnnen1lem3  11760  rpnnen1lem5  11762  rpnnen1lem1OLD  11765  rpnnen1lem3OLD  11766  rpnnen1lem5OLD  11768  seqof  12798  seqof2  12799  rlim2  14161  ello1mpt  14186  o1compt  14252  sumrblem  14375  fsumcvg  14376  summolem2a  14379  fsum  14384  fsumcvg2  14391  fsumadd  14403  isummulc2  14421  fsummulc2  14444  fsumrelem  14466  prodrblem  14584  fprodcvg  14585  prodmolem2a  14589  zprod  14592  fprod  14596  fprodmul  14615  fproddiv  14616  iserodd  15464  prmrec  15550  prdsbas3  16062  prdsdsval2  16065  invfuc  16555  yonedalem4c  16838  gsumconst  18255  prdsgsum  18298  gsumdixp  18530  evlslem4  19427  elptr2  21287  ptunimpt  21308  ptcldmpt  21327  ptclsg  21328  txcnp  21333  ptcnplem  21334  cnmpt11  21376  cnmpt1t  21378  cnmptk2  21399  xkocnv  21527  flfcnp2  21721  ustn0  21934  utopsnneiplem  21961  ucnima  21995  iccpnfcnv  22651  ovolctb  23165  ovoliunlem1  23177  ovoliun2  23181  ovolshftlem1  23184  ovolscalem1  23188  voliun  23229  ioombl1lem3  23235  ioombl1lem4  23236  uniioombllem2  23257  mbfeqalem  23315  mbfpos  23324  mbfposr  23325  mbfposb  23326  mbfsup  23337  mbfinf  23338  mbflim  23341  i1fposd  23380  itg1climres  23387  mbfi1fseqlem4  23391  mbfi1fseqlem5  23392  mbfi1fseqlem6  23393  itg2split  23422  itg2mono  23426  itg2cnlem1  23434  isibl2  23439  itgmpt  23455  itgeqa  23486  itggt0  23514  itgcn  23515  limcmpt  23553  dvlipcn  23661  lhop2  23682  dvfsumabs  23690  itgparts  23714  itgsubstlem  23715  itgsubst  23716  elplyd  23862  coeeulem  23884  coeeq2  23902  dvply1  23943  plyremlem  23963  ulmss  24055  ulmdvlem1  24058  mtest  24062  itgulm2  24067  radcnvlem1  24071  pserulm  24080  leibpi  24569  rlimcnp  24592  o1cxp  24601  lgamgulmlem2  24656  lgamgulmlem6  24660  lgamgulm2  24662  sqff1o  24808  lgseisenlem2  25001  dchrvmasumlem1  25084  frgrncvvdeqlem6  27032  ubthlem1  27575  cnlnadjlem5  28779  xppreima2  29292  abfmpunirn  29294  aciunf1lem  29304  fpwrelmap  29351  fimaproj  29682  xrmulc1cn  29758  esumpcvgval  29921  esumsup  29932  voliune  30073  eulerpartgbij  30215  signsplypnf  30407  iscvm  30949  mclsrcl  31166  f1omptsnlem  32815  matunitlindflem2  33038  itg2addnclem  33093  itggt0cn  33114  ftc1anclem5  33121  elrfirn2  36739  eq0rabdioph  36820  monotoddzz  36988  aomclem2  37105  refsumcn  38672  refsum2cnlem1  38679  fvmpt2bd  38824  wessf1ornlem  38845  fompt  38853  projf1o  38860  choicefi  38866  axccdom  38890  fvmpt4  38921  feqresmpt2  38936  fsumsermpt  39215  fmuldfeqlem1  39218  fmuldfeq  39219  climneg  39246  climdivf  39248  mullimc  39252  idlimc  39262  sumnnodd  39266  neglimc  39283  addlimc  39284  0ellimcdiv  39285  climfveqmpt2  39329  climeqmpt  39333  limsupequzmptlem  39364  cncfmptssg  39386  cncfshift  39390  icccncfext  39404  cncfiooicclem1  39410  fprodsubrecnncnvlem  39425  fprodaddrecnncnvlem  39427  ioodvbdlimc1lem2  39453  ioodvbdlimc2lem  39455  dvnmptdivc  39459  dvnmul  39464  dvnprodlem2  39468  itgsin0pilem1  39472  ibliccsinexp  39473  itgsinexplem1  39476  itgsinexp  39477  ditgeqiooicc  39483  itgsubsticclem  39498  itgioocnicc  39500  stoweidlem2  39526  stoweidlem11  39535  stoweidlem12  39536  stoweidlem16  39540  stoweidlem17  39541  stoweidlem18  39542  stoweidlem19  39543  stoweidlem20  39544  stoweidlem21  39545  stoweidlem22  39546  stoweidlem23  39547  stoweidlem27  39551  stoweidlem31  39555  stoweidlem34  39558  stoweidlem36  39560  stoweidlem40  39564  stoweidlem41  39565  stoweidlem42  39566  stoweidlem48  39572  stoweidlem55  39579  stoweidlem59  39583  stoweidlem62  39586  stirlinglem3  39600  stirlinglem8  39605  stirlinglem14  39611  stirlinglem15  39612  stirlingr  39614  dirkeritg  39626  dirkercncflem2  39628  fourierdlem14  39645  fourierdlem31  39662  fourierdlem41  39672  fourierdlem48  39678  fourierdlem49  39679  fourierdlem50  39680  fourierdlem51  39681  fourierdlem56  39686  fourierdlem60  39690  fourierdlem61  39691  fourierdlem66  39696  fourierdlem70  39700  fourierdlem71  39701  fourierdlem73  39703  fourierdlem74  39704  fourierdlem75  39705  fourierdlem76  39706  fourierdlem77  39707  fourierdlem78  39708  fourierdlem81  39711  fourierdlem83  39713  fourierdlem84  39714  fourierdlem85  39715  fourierdlem87  39717  fourierdlem88  39718  fourierdlem89  39719  fourierdlem91  39721  fourierdlem92  39722  fourierdlem93  39723  fourierdlem95  39725  fourierdlem97  39727  fourierdlem101  39731  fourierdlem103  39733  fourierdlem104  39734  fourierdlem111  39741  fourierdlem112  39742  sqwvfoura  39752  sqwvfourb  39753  fouriersw  39755  elaa2lem  39757  etransclem4  39762  etransclem13  39771  etransclem35  39793  etransclem46  39804  etransclem48  39806  sge0revalmpt  39902  sge0fsummpt  39914  sge0iunmptlemfi  39937  sge0iunmptlemre  39939  sge0ltfirpmpt2  39950  sge0fsummptf  39960  nnfoctbdjlem  39979  iundjiun  39984  meaiunlelem  39992  meaiuninclem  40004  omeiunlempt  40041  carageniuncllem2  40043  caratheodorylem2  40048  0ome  40050  isomenndlem  40051  hoicvr  40069  hoicvrrex  40077  ovn0lem  40086  ovnsubaddlem1  40091  hoidmvlelem2  40117  hoidmvlelem3  40118  ovnhoilem2  40123  hoicoto2  40126  hoi2toco  40128  ovnlecvr2  40131  ovncvr2  40132  ovnsubadd2lem  40166  ovolval5lem2  40174  ovnovollem1  40177  ovnovollem2  40178  vonioolem1  40201  smfaddlem1  40278  smflimlem2  40287  smflimmpt  40323  smfsupmpt  40328  smfinfmpt  40332  smflimsuplem2  40334  smflimsuplem4  40336  smflimsuplem5  40337  smflimsupmpt  40342  aacllem  41850
  Copyright terms: Public domain W3C validator