Theorem fvmpt2 6996

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 6995	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = ( I ‘𝐵))
3		fvi 6954	. 2 ⊢ (𝐵 ∈ 𝐶 → ( I ‘𝐵) = 𝐵)
4	2, 3	sylan9eq 2790	1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5201   I cid 5547  ‘cfv 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fv 6538

This theorem is referenced by:  fvmptss  6997  fvmpt2d  6998  fvmptd3f  7000  mpteqb  7004  fvmptt  7005  fvmptf  7006  fnmptfvd  7030  ralrnmptw  7083  ralrnmpt  7085  fompt  7107  fmptco  7118  f1mpt  7253  offval2  7689  ofrfval2  7690  fimaproj  8132  mptelixpg  8947  dom2lem  9004  mapxpen  9155  xpmapenlem  9156  cnfcom3clem  9717  tcvalg  9750  rankf  9806  infxpenc2lem2  10032  dfac8clem  10044  acni2  10058  acnlem  10060  fin23lem32  10356  axcc2lem  10448  axcc3  10450  domtriomlem  10454  ac6num  10491  konigthlem  10580  rpnnen1lem1  12992  rpnnen1lem3  12993  rpnnen1lem5  12995  seqof  14075  seqof2  14076  rlim2  15510  ello1mpt  15535  o1compt  15601  sumrblem  15725  fsumcvg  15726  summolem2a  15729  fsum  15734  fsumcvg2  15741  fsumadd  15754  isummulc2  15776  fsummulc2  15798  fsumrelem  15821  prodrblem  15943  fprodcvg  15944  prodmolem2a  15948  zprod  15951  fprod  15955  fprodmul  15974  fproddiv  15975  iserodd  16853  prmrec  16940  prdsbas3  17493  prdsdsval2  17496  invfuc  17988  yonedalem4c  18287  smndex1n0mnd  18888  gsumconst  19913  prdsgsum  19960  gsumdixp  20277  evlslem4  22032  elptr2  23510  ptunimpt  23531  ptcldmpt  23550  ptclsg  23551  txcnp  23556  ptcnplem  23557  cnmpt11  23599  cnmpt1t  23601  cnmptk2  23622  xkocnv  23750  flfcnp2  23943  ustn0  24157  utopsnneiplem  24184  ucnima  24217  iccpnfcnv  24891  ovolctb  25441  ovoliunlem1  25453  ovoliun2  25457  ovolshftlem1  25460  ovolscalem1  25464  voliun  25505  ioombl1lem3  25511  ioombl1lem4  25512  uniioombllem2  25534  mbfeqalem1  25592  mbfpos  25602  mbfposr  25603  mbfposb  25604  mbfsup  25615  mbfinf  25616  mbflim  25619  i1fposd  25658  itg1climres  25665  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1fseqlem6  25671  itg2split  25700  itg2mono  25704  itg2cnlem1  25712  isibl2  25717  itgmpt  25734  itgeqa  25765  itggt0  25795  itgcn  25796  limcmpt  25834  dvlipcn  25949  lhop2  25970  dvfsumabs  25979  itgparts  26004  itgsubstlem  26005  itgsubst  26006  elplyd  26157  coeeulem  26179  coeeq2  26197  dvply1  26241  plyremlem  26262  ulmss  26356  ulmdvlem1  26359  mtest  26363  itgulm2  26368  radcnvlem1  26372  pserulm  26381  leibpi  26902  rlimcnp  26925  o1cxp  26935  lgamgulmlem2  26990  lgamgulmlem6  26994  lgamgulm2  26996  sqff1o  27142  lgseisenlem2  27337  dchrvmasumlem1  27456  frgrncvvdeqlem5  30230  ubthlem1  30797  cnlnadjlem5  31998  xppreima2  32575  abfmpunirn  32576  aciunf1lem  32586  suppovss  32604  fpwrelmap  32656  nsgmgc  33373  zringfrac  33515  algextdeglem6  33702  xrmulc1cn  33907  esumpcvgval  34055  esumsup  34066  voliune  34206  eulerpartgbij  34350  signsplypnf  34528  wevgblacfn  35077  iscvm  35227  mclsrcl  35529  f1omptsnlem  37300  matunitlindflem2  37587  itg2addnclem  37641  itggt0cn  37660  ftc1anclem5  37667  pwsgprod  42514  elrfirn2  42666  eq0rabdioph  42746  monotoddzz  42914  aomclem2  43026  refsumcn  45002  refsum2cnlem1  45009  fvmpt2bd  45142  choicefi  45172  axccdom  45194  fvmpt4  45210  fsumsermpt  45556  fmuldfeqlem1  45559  fmuldfeq  45560  climneg  45587  climdivf  45589  mullimc  45593  idlimc  45603  sumnnodd  45607  neglimc  45624  addlimc  45625  0ellimcdiv  45626  climfveqmpt2  45670  climeqmpt  45674  limsupequzmptlem  45705  liminfvalxr  45760  xlimmnfmpt  45820  xlimpnfmpt  45821  cncfmptssg  45848  cncfshift  45851  icccncfext  45864  cncfiooicclem1  45870  fprodsubrecnncnvlem  45884  fprodaddrecnncnvlem  45886  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnmptdivc  45915  dvnmul  45920  dvnprodlem2  45924  itgsin0pilem1  45927  ibliccsinexp  45928  itgsinexplem1  45931  itgsinexp  45932  ditgeqiooicc  45937  itgsubsticclem  45952  itgioocnicc  45954  stoweidlem2  45979  stoweidlem11  45988  stoweidlem12  45989  stoweidlem16  45993  stoweidlem17  45994  stoweidlem18  45995  stoweidlem19  45996  stoweidlem20  45997  stoweidlem21  45998  stoweidlem22  45999  stoweidlem23  46000  stoweidlem27  46004  stoweidlem31  46008  stoweidlem34  46011  stoweidlem36  46013  stoweidlem40  46017  stoweidlem41  46018  stoweidlem42  46019  stoweidlem48  46025  stoweidlem55  46032  stoweidlem59  46036  stoweidlem62  46039  stirlinglem3  46053  stirlinglem8  46058  stirlinglem14  46064  stirlinglem15  46065  stirlingr  46067  dirkeritg  46079  dirkercncflem2  46081  fourierdlem14  46098  fourierdlem31  46115  fourierdlem41  46125  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem51  46134  fourierdlem56  46139  fourierdlem60  46143  fourierdlem61  46144  fourierdlem66  46149  fourierdlem70  46153  fourierdlem71  46154  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem77  46160  fourierdlem78  46161  fourierdlem81  46164  fourierdlem83  46166  fourierdlem84  46167  fourierdlem85  46168  fourierdlem87  46170  fourierdlem88  46171  fourierdlem89  46172  fourierdlem91  46174  fourierdlem92  46175  fourierdlem93  46176  fourierdlem95  46178  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  elaa2lem  46210  etransclem4  46215  etransclem13  46224  etransclem35  46246  etransclem46  46257  etransclem48  46259  sge0revalmpt  46355  sge0fsummpt  46367  sge0iunmptlemfi  46390  sge0iunmptlemre  46392  sge0ltfirpmpt2  46403  sge0fsummptf  46413  nnfoctbdjlem  46432  iundjiun  46437  meaiunlelem  46445  meaiuninclem  46457  meaiuninc3v  46461  omeiunlempt  46497  carageniuncllem2  46499  caratheodorylem2  46504  0ome  46506  isomenndlem  46507  hoicvr  46525  hoicvrrex  46533  ovn0lem  46542  ovnsubaddlem1  46547  hoidmvlelem2  46573  hoidmvlelem3  46574  ovnhoilem2  46579  hoicoto2  46582  hoi2toco  46584  ovnlecvr2  46587  ovncvr2  46588  ovnsubadd2lem  46622  ovolval5lem2  46630  ovnovollem1  46633  ovnovollem2  46634  vonioolem1  46657  smfaddlem1  46740  smflimlem2  46749  smflimmpt  46787  smflimsuplem2  46798  smflimsuplem4  46800  smflimsuplem5  46801  smflimsupmpt  46806  smfliminfmpt  46809  smfsupdmmbllem  46821  finfdm  46823  smfinfdmmbllem  46825  setrec2mpt  49509  aacllem  49613