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

Theorem fvmpt2 6772
 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 6771 . 2 (𝑥𝐴 → (𝐹𝑥) = ( I ‘𝐵))
3 fvi 6733 . 2 (𝐵𝐶 → ( I ‘𝐵) = 𝐵)
42, 3sylan9eq 2874 1 ((𝑥𝐴𝐵𝐶) → (𝐹𝑥) = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1531   ∈ wcel 2108   ↦ cmpt 5137   I cid 5452  ‘cfv 6348 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fv 6356 This theorem is referenced by:  fvmptss  6773  fvmpt2d  6774  fvmptd3f  6776  mpteqb  6780  fvmptt  6781  fvmptf  6782  fnmptfvd  6804  ralrnmptw  6853  ralrnmpt  6855  fmptco  6884  f1mpt  7011  offval2  7418  ofrfval2  7419  fimaproj  7821  mptelixpg  8491  dom2lem  8541  mapxpen  8675  xpmapenlem  8676  cnfcom3clem  9160  tcvalg  9172  rankf  9215  infxpenc2lem2  9438  dfac8clem  9450  acni2  9464  acnlem  9466  fin23lem32  9758  axcc2lem  9850  axcc3  9852  domtriomlem  9856  ac6num  9893  konigthlem  9982  rpnnen1lem1  12369  rpnnen1lem3  12370  rpnnen1lem5  12372  seqof  13419  seqof2  13420  rlim2  14845  ello1mpt  14870  o1compt  14936  sumrblem  15060  fsumcvg  15061  summolem2a  15064  fsum  15069  fsumcvg2  15076  fsumadd  15088  isummulc2  15109  fsummulc2  15131  fsumrelem  15154  prodrblem  15275  fprodcvg  15276  prodmolem2a  15280  zprod  15283  fprod  15287  fprodmul  15306  fproddiv  15307  iserodd  16164  prmrec  16250  prdsbas3  16746  prdsdsval2  16749  invfuc  17236  yonedalem4c  17519  smndex1n0mnd  18069  gsumconst  19046  prdsgsum  19093  gsumdixp  19351  evlslem4  20280  elptr2  22174  ptunimpt  22195  ptcldmpt  22214  ptclsg  22215  txcnp  22220  ptcnplem  22221  cnmpt11  22263  cnmpt1t  22265  cnmptk2  22286  xkocnv  22414  flfcnp2  22607  ustn0  22821  utopsnneiplem  22848  ucnima  22882  iccpnfcnv  23540  ovolctb  24083  ovoliunlem1  24095  ovoliun2  24099  ovolshftlem1  24102  ovolscalem1  24106  voliun  24147  ioombl1lem3  24153  ioombl1lem4  24154  uniioombllem2  24176  mbfeqalem1  24234  mbfpos  24244  mbfposr  24245  mbfposb  24246  mbfsup  24257  mbfinf  24258  mbflim  24261  i1fposd  24300  itg1climres  24307  mbfi1fseqlem4  24311  mbfi1fseqlem5  24312  mbfi1fseqlem6  24313  itg2split  24342  itg2mono  24346  itg2cnlem1  24354  isibl2  24359  itgmpt  24375  itgeqa  24406  itggt0  24434  itgcn  24435  limcmpt  24473  dvlipcn  24583  lhop2  24604  dvfsumabs  24612  itgparts  24636  itgsubstlem  24637  itgsubst  24638  elplyd  24784  coeeulem  24806  coeeq2  24824  dvply1  24865  plyremlem  24885  ulmss  24977  ulmdvlem1  24980  mtest  24984  itgulm2  24989  radcnvlem1  24993  pserulm  25002  leibpi  25512  rlimcnp  25535  o1cxp  25544  lgamgulmlem2  25599  lgamgulmlem6  25603  lgamgulm2  25605  sqff1o  25751  lgseisenlem2  25944  dchrvmasumlem1  26063  frgrncvvdeqlem5  28074  ubthlem1  28639  cnlnadjlem5  29840  xppreima2  30387  abfmpunirn  30389  aciunf1lem  30399  suppovss  30418  fpwrelmap  30461  xrmulc1cn  31166  esumpcvgval  31330  esumsup  31341  voliune  31481  eulerpartgbij  31623  signsplypnf  31813  iscvm  32499  mclsrcl  32801  f1omptsnlem  34609  matunitlindflem2  34881  itg2addnclem  34935  itggt0cn  34956  ftc1anclem5  34963  elrfirn2  39284  eq0rabdioph  39364  monotoddzz  39531  aomclem2  39646  refsumcn  41278  refsum2cnlem1  41285  fvmpt2bd  41416  fompt  41443  choicefi  41453  axccdom  41477  fvmpt4  41498  fsumsermpt  41850  fmuldfeqlem1  41853  fmuldfeq  41854  climneg  41881  climdivf  41883  mullimc  41887  idlimc  41897  sumnnodd  41901  neglimc  41918  addlimc  41919  0ellimcdiv  41920  climfveqmpt2  41964  climeqmpt  41968  limsupequzmptlem  41999  liminfvalxr  42054  xlimmnfmpt  42114  xlimpnfmpt  42115  cncfmptssg  42143  cncfshift  42147  icccncfext  42160  cncfiooicclem1  42166  fprodsubrecnncnvlem  42181  fprodaddrecnncnvlem  42183  ioodvbdlimc1lem2  42207  ioodvbdlimc2lem  42209  dvnmptdivc  42213  dvnmul  42218  dvnprodlem2  42222  itgsin0pilem1  42225  ibliccsinexp  42226  itgsinexplem1  42229  itgsinexp  42230  ditgeqiooicc  42235  itgsubsticclem  42250  itgioocnicc  42252  stoweidlem2  42278  stoweidlem11  42287  stoweidlem12  42288  stoweidlem16  42292  stoweidlem17  42293  stoweidlem18  42294  stoweidlem19  42295  stoweidlem20  42296  stoweidlem21  42297  stoweidlem22  42298  stoweidlem23  42299  stoweidlem27  42303  stoweidlem31  42307  stoweidlem34  42310  stoweidlem36  42312  stoweidlem40  42316  stoweidlem41  42317  stoweidlem42  42318  stoweidlem48  42324  stoweidlem55  42331  stoweidlem59  42335  stoweidlem62  42338  stirlinglem3  42352  stirlinglem8  42357  stirlinglem14  42363  stirlinglem15  42364  stirlingr  42366  dirkeritg  42378  dirkercncflem2  42380  fourierdlem14  42397  fourierdlem31  42414  fourierdlem41  42424  fourierdlem48  42430  fourierdlem49  42431  fourierdlem50  42432  fourierdlem51  42433  fourierdlem56  42438  fourierdlem60  42442  fourierdlem61  42443  fourierdlem66  42448  fourierdlem70  42452  fourierdlem71  42453  fourierdlem73  42455  fourierdlem74  42456  fourierdlem75  42457  fourierdlem76  42458  fourierdlem77  42459  fourierdlem78  42460  fourierdlem81  42463  fourierdlem83  42465  fourierdlem84  42466  fourierdlem85  42467  fourierdlem87  42469  fourierdlem88  42470  fourierdlem89  42471  fourierdlem91  42473  fourierdlem92  42474  fourierdlem93  42475  fourierdlem95  42477  fourierdlem97  42479  fourierdlem101  42483  fourierdlem103  42485  fourierdlem104  42486  fourierdlem111  42493  fourierdlem112  42494  sqwvfoura  42504  sqwvfourb  42505  fouriersw  42507  elaa2lem  42509  etransclem4  42514  etransclem13  42523  etransclem35  42545  etransclem46  42556  etransclem48  42558  sge0revalmpt  42651  sge0fsummpt  42663  sge0iunmptlemfi  42686  sge0iunmptlemre  42688  sge0ltfirpmpt2  42699  sge0fsummptf  42709  nnfoctbdjlem  42728  iundjiun  42733  meaiunlelem  42741  meaiuninclem  42753  meaiuninc3v  42757  omeiunlempt  42793  carageniuncllem2  42795  caratheodorylem2  42800  0ome  42802  isomenndlem  42803  hoicvr  42821  hoicvrrex  42829  ovn0lem  42838  ovnsubaddlem1  42843  hoidmvlelem2  42869  hoidmvlelem3  42870  ovnhoilem2  42875  hoicoto2  42878  hoi2toco  42880  ovnlecvr2  42883  ovncvr2  42884  ovnsubadd2lem  42918  ovolval5lem2  42926  ovnovollem1  42929  ovnovollem2  42930  vonioolem1  42953  smfaddlem1  43030  smflimlem2  43039  smflimmpt  43075  smfsupmpt  43080  smfinfmpt  43084  smflimsuplem2  43086  smflimsuplem4  43088  smflimsuplem5  43089  smflimsupmpt  43094  smfliminfmpt  43097  aacllem  44893
 Copyright terms: Public domain W3C validator