Theorem fvmpt2 7028

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

Step	Hyp	Ref	Expression
1		mptrcl.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	fvmpt2i 7027	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = ( I ‘𝐵))
3		fvi 6984	. 2 ⊢ (𝐵 ∈ 𝐶 → ( I ‘𝐵) = 𝐵)
4	2, 3	sylan9eq 2818	1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ↦ cmpt 5189   I cid 5549  ‘cfv 6558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fv 6566

This theorem is used by:  fvmptss  7029  fvmpt2d  7030  fvmptd3f  7032  mpteqb  7036  fvmptt  7037  fvmptf  7038  fnmptfvd  7063  ralrnmptw  7118  ralrnmpt  7120  fompt  7142  fmptco  7154  f1mpt  7288  offval2  7737  ofrfval2  7738  fimaproj  8179  mptelixpg  8991  dom2lem  9047  mapxpen  9190  xpmapenlem  9191  cnfcom3clem  9733  tcvalg  9764  rankf  9829  infxpenc2lem2  10126  dfac8clem  10138  acni2  10152  acnlem  10154  fin23lem32  10449  axcc2lem  10541  axcc3  10543  domtriomlem  10547  ac6num  10584  konigthlem  10680  rpnnen1lem1  13133  rpnnen1lem3  13134  rpnnen1lem5  13136  seqof  14229  seqof2  14230  rlim2  15692  ello1mpt  15717  o1compt  15783  sumrblem  15906  fsumcvg  15907  summolem2a  15910  fsum  15915  fsumcvg2  15922  fsumadd  15935  isummulc2  15957  fsummulc2  15979  fsumrelem  16003  prodrblem  16125  fprodcvg  16126  prodmolem2a  16130  zprod  16133  fprod  16137  fprodmul  16156  fproddiv  16157  iserodd  17042  prmrec  17129  prdsbas3  17681  prdsdsval2  17684  invfuc  18181  yonedalem4c  18480  smndex1n0mnd  19140  gsumconst  20178  prdsgsum  20225  gsumdixp  20578  pwsgprod  20589  evlslem4  22415  matunitlindflem2  23025  elptr2  23923  ptunimpt  23944  ptcldmpt  23963  ptclsg  23964  txcnp  23969  ptcnplem  23970  cnmpt11  24012  cnmpt1t  24014  cnmptk2  24035  xkocnv  24163  flfcnp2  24356  ustn0  24570  utopsnneiplem  24596  ucnima  24629  iccpnfcnv  25295  ovolctb  25841  ovoliunlem1  25853  ovoliun2  25857  ovolshftlem1  25860  ovolscalem1  25864  voliun  25905  ioombl1lem3  25911  ioombl1lem4  25912  uniioombllem2  25934  mbfeqalem1  25992  mbfpos  26002  mbfposr  26003  mbfposb  26004  mbfsup  26015  mbfinf  26016  mbflim  26019  i1fposd  26058  itg1climres  26065  mbfi1fseqlem4  26069  mbfi1fseqlem5  26070  mbfi1fseqlem6  26071  itg2split  26100  itg2mono  26104  itg2cnlem1  26112  isibl2  26117  itgmpt  26133  itgeqa  26164  itggt0  26194  itgcn  26195  limcmpt  26233  dvlipcn  26344  lhop2  26365  dvfsumabs  26373  itgparts  26397  itgsubstlem  26398  itgsubst  26399  elplyd  26550  coeeulem  26573  coeeq2  26591  dvply1  26635  plyremlem  26655  ulmss  26754  ulmdvlem1  26757  mtest  26761  itgulm2  26766  radcnvlem1  26770  pserulm  26779  leibpi  27300  rlimcnp  27323  o1cxp  27332  lgamgulmlem2  27387  lgamgulmlem6  27391  lgamgulm2  27393  sqff1o  27539  lgseisenlem2  27733  dchrvmasumlem1  27852  frgrncvvdeqlem5  30934  ubthlem1  31502  cnlnadjlem5  32703  xppreima2  33317  abfmpunirn  33318  aciunf1lem  33328  suppovss  33345  fpwrelmap  33395  suppgsumssiun  33703  nsgmgc  34033  zringfrac  34156  extdgfialglem2  34395  algextdeglem6  34424  xrmulc1cn  34632  esumpcvgval  34780  esumsup  34791  voliune  34932  eulerpartgbij  35074  signsplypnf  35249  wevgblacfn  36039  iscvm  36191  mclsrcl  36493  f1omptsnlem  38451  itg2addnclem  38781  itggt0cn  38800  ftc1anclem5  38807  elrfirn2  43900  eq0rabdioph  43980  monotoddzz  44143  aomclem2  44250  refsumcn  46252  refsum2cnlem1  46259  fvmpt2bd  46390  choicefi  46419  axccdom  46440  fvmpt4  46455  fsumsermpt  46796  fmuldfeqlem1  46799  fmuldfeq  46800  climneg  46827  climdivf  46829  mullimc  46833  idlimc  46843  sumnnodd  46847  neglimc  46862  addlimc  46863  0ellimcdiv  46864  climfveqmpt2  46908  climeqmpt  46912  limsupequzmptlem  46943  liminfvalxr  46998  xlimmnfmpt  47058  xlimpnfmpt  47059  cncfmptssg  47086  cncfshift  47089  icccncfext  47102  cncfiooicclem1  47108  fprodsubrecnncnvlem  47122  fprodaddrecnncnvlem  47124  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  dvnmptdivc  47153  dvnmul  47158  dvnprodlem2  47162  itgsin0pilem1  47165  ibliccsinexp  47166  itgsinexplem1  47169  itgsinexp  47170  ditgeqiooicc  47175  itgsubsticclem  47190  itgioocnicc  47192  stoweidlem2  47217  stoweidlem11  47226  stoweidlem12  47227  stoweidlem16  47231  stoweidlem17  47232  stoweidlem18  47233  stoweidlem19  47234  stoweidlem20  47235  stoweidlem21  47236  stoweidlem22  47237  stoweidlem23  47238  stoweidlem27  47242  stoweidlem31  47246  stoweidlem34  47249  stoweidlem36  47251  stoweidlem40  47255  stoweidlem41  47256  stoweidlem42  47257  stoweidlem48  47263  stoweidlem55  47270  stoweidlem59  47274  stoweidlem62  47277  stirlinglem3  47291  stirlinglem8  47296  stirlinglem14  47302  stirlinglem15  47303  stirlingr  47305  dirkeritg  47317  dirkercncflem2  47319  fourierdlem14  47336  fourierdlem31  47353  fourierdlem41  47363  fourierdlem48  47369  fourierdlem49  47370  fourierdlem50  47371  fourierdlem51  47372  fourierdlem56  47377  fourierdlem60  47381  fourierdlem61  47382  fourierdlem66  47387  fourierdlem70  47391  fourierdlem71  47392  fourierdlem73  47394  fourierdlem74  47395  fourierdlem75  47396  fourierdlem76  47397  fourierdlem77  47398  fourierdlem78  47399  fourierdlem81  47402  fourierdlem83  47404  fourierdlem84  47405  fourierdlem85  47406  fourierdlem87  47408  fourierdlem88  47409  fourierdlem89  47410  fourierdlem91  47412  fourierdlem92  47413  fourierdlem93  47414  fourierdlem95  47416  fourierdlem97  47418  fourierdlem101  47422  fourierdlem103  47424  fourierdlem104  47425  fourierdlem111  47432  fourierdlem112  47433  sqwvfoura  47443  sqwvfourb  47444  fouriersw  47446  elaa2lem  47448  etransclem4  47453  etransclem13  47462  etransclem35  47484  etransclem46  47495  etransclem48  47497  sge0revalmpt  47593  sge0fsummpt  47605  sge0iunmptlemfi  47628  sge0iunmptlemre  47630  sge0ltfirpmpt2  47641  sge0fsummptf  47651  nnfoctbdjlem  47670  iundjiun  47675  meaiunlelem  47683  meaiuninclem  47695  meaiuninc3v  47699  omeiunlempt  47735  carageniuncllem2  47737  caratheodorylem2  47742  0ome  47744  isomenndlem  47745  hoicvr  47763  hoicvrrex  47771  ovn0lem  47780  ovnsubaddlem1  47785  hoidmvlelem2  47811  hoidmvlelem3  47812  ovnhoilem2  47817  hoicoto2  47820  hoi2toco  47822  ovnlecvr2  47825  ovncvr2  47826  ovnsubadd2lem  47860  ovolval5lem2  47868  ovnovollem1  47871  ovnovollem2  47872  vonioolem1  47895  smfaddlem1  47978  smflimlem2  47987  smflimmpt  48025  smflimsuplem2  48036  smflimsuplem4  48038  smflimsuplem5  48039  smflimsupmpt  48044  smfliminfmpt  48047  smfsupdmmbllem  48059  finfdm  48061  smfinfdmmbllem  48063  setrec2mpt  51070  aacllem  51219