Theorem fvmpt2 7005

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ↦ cmpt 5185   I cid 5544  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is used by:  fvmptss  7006  fvmpt2d  7007  fvmptd3f  7009  mpteqb  7013  fvmptt  7014  fvmptf  7015  fnmptfvd  7040  ralrnmptw  7094  ralrnmpt  7096  fompt  7118  fmptco  7130  f1mpt  7265  offval2  7713  ofrfval2  7714  fimaproj  8154  mptelixpg  8966  dom2lem  9022  mapxpen  9165  xpmapenlem  9166  cnfcom3clem  9709  tcvalg  9740  rankf  9805  infxpenc2lem2  10102  dfac8clem  10114  acni2  10128  acnlem  10130  fin23lem32  10425  axcc2lem  10517  axcc3  10519  domtriomlem  10523  ac6num  10560  konigthlem  10656  rpnnen1lem1  13109  rpnnen1lem3  13110  rpnnen1lem5  13112  seqof  14205  seqof2  14206  rlim2  15668  ello1mpt  15693  o1compt  15759  sumrblem  15882  fsumcvg  15883  summolem2a  15886  fsum  15891  fsumcvg2  15898  fsumadd  15911  isummulc2  15933  fsummulc2  15955  fsumrelem  15979  prodrblem  16101  fprodcvg  16102  prodmolem2a  16106  zprod  16109  fprod  16113  fprodmul  16132  fproddiv  16133  iserodd  17018  prmrec  17105  prdsbas3  17657  prdsdsval2  17660  invfuc  18157  yonedalem4c  18456  smndex1n0mnd  19116  gsumconst  20153  prdsgsum  20200  gsumdixp  20553  pwsgprod  20564  evlslem4  22390  matunitlindflem2  23000  elptr2  23898  ptunimpt  23919  ptcldmpt  23938  ptclsg  23939  txcnp  23944  ptcnplem  23945  cnmpt11  23987  cnmpt1t  23989  cnmptk2  24010  xkocnv  24138  flfcnp2  24331  ustn0  24545  utopsnneiplem  24571  ucnima  24604  iccpnfcnv  25270  ovolctb  25816  ovoliunlem1  25828  ovoliun2  25832  ovolshftlem1  25835  ovolscalem1  25839  voliun  25880  ioombl1lem3  25886  ioombl1lem4  25887  uniioombllem2  25909  mbfeqalem1  25967  mbfpos  25977  mbfposr  25978  mbfposb  25979  mbfsup  25990  mbfinf  25991  mbflim  25994  i1fposd  26033  itg1climres  26040  mbfi1fseqlem4  26044  mbfi1fseqlem5  26045  mbfi1fseqlem6  26046  itg2split  26075  itg2mono  26079  itg2cnlem1  26087  isibl2  26092  itgmpt  26108  itgeqa  26139  itggt0  26169  itgcn  26170  limcmpt  26208  dvlipcn  26319  lhop2  26340  dvfsumabs  26348  itgparts  26372  itgsubstlem  26373  itgsubst  26374  elplyd  26525  coeeulem  26548  coeeq2  26566  dvply1  26610  plyremlem  26630  ulmss  26729  ulmdvlem1  26732  mtest  26736  itgulm2  26741  radcnvlem1  26745  pserulm  26754  leibpi  27275  rlimcnp  27298  o1cxp  27307  lgamgulmlem2  27362  lgamgulmlem6  27366  lgamgulm2  27368  sqff1o  27514  lgseisenlem2  27708  dchrvmasumlem1  27827  frgrncvvdeqlem5  30909  ubthlem1  31477  cnlnadjlem5  32678  xppreima2  33292  abfmpunirn  33293  aciunf1lem  33303  suppovss  33321  fpwrelmap  33371  suppgsumssiun  33679  nsgmgc  34009  zringfrac  34132  extdgfialglem2  34371  algextdeglem6  34400  xrmulc1cn  34608  esumpcvgval  34756  esumsup  34767  voliune  34908  eulerpartgbij  35050  signsplypnf  35225  wevgblacfn  35958  iscvm  36110  mclsrcl  36412  f1omptsnlem  38352  itg2addnclem  38682  itggt0cn  38701  ftc1anclem5  38708  elrfirn2  43800  eq0rabdioph  43880  monotoddzz  44043  aomclem2  44150  refsumcn  46140  refsum2cnlem1  46147  fvmpt2bd  46278  choicefi  46307  axccdom  46328  fvmpt4  46343  fsumsermpt  46684  fmuldfeqlem1  46687  fmuldfeq  46688  climneg  46715  climdivf  46717  mullimc  46721  idlimc  46731  sumnnodd  46735  neglimc  46750  addlimc  46751  0ellimcdiv  46752  climfveqmpt2  46796  climeqmpt  46800  limsupequzmptlem  46831  liminfvalxr  46886  xlimmnfmpt  46946  xlimpnfmpt  46947  cncfmptssg  46974  cncfshift  46977  icccncfext  46990  cncfiooicclem1  46996  fprodsubrecnncnvlem  47010  fprodaddrecnncnvlem  47012  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  dvnmptdivc  47041  dvnmul  47046  dvnprodlem2  47050  itgsin0pilem1  47053  ibliccsinexp  47054  itgsinexplem1  47057  itgsinexp  47058  ditgeqiooicc  47063  itgsubsticclem  47078  itgioocnicc  47080  stoweidlem2  47105  stoweidlem11  47114  stoweidlem12  47115  stoweidlem16  47119  stoweidlem17  47120  stoweidlem18  47121  stoweidlem19  47122  stoweidlem20  47123  stoweidlem21  47124  stoweidlem22  47125  stoweidlem23  47126  stoweidlem27  47130  stoweidlem31  47134  stoweidlem34  47137  stoweidlem36  47139  stoweidlem40  47143  stoweidlem41  47144  stoweidlem42  47145  stoweidlem48  47151  stoweidlem55  47158  stoweidlem59  47162  stoweidlem62  47165  stirlinglem3  47179  stirlinglem8  47184  stirlinglem14  47190  stirlinglem15  47191  stirlingr  47193  dirkeritg  47205  dirkercncflem2  47207  fourierdlem14  47224  fourierdlem31  47241  fourierdlem41  47251  fourierdlem48  47257  fourierdlem49  47258  fourierdlem50  47259  fourierdlem51  47260  fourierdlem56  47265  fourierdlem60  47269  fourierdlem61  47270  fourierdlem66  47275  fourierdlem70  47279  fourierdlem71  47280  fourierdlem73  47282  fourierdlem74  47283  fourierdlem75  47284  fourierdlem76  47285  fourierdlem77  47286  fourierdlem78  47287  fourierdlem81  47290  fourierdlem83  47292  fourierdlem84  47293  fourierdlem85  47294  fourierdlem87  47296  fourierdlem88  47297  fourierdlem89  47298  fourierdlem91  47300  fourierdlem92  47301  fourierdlem93  47302  fourierdlem95  47304  fourierdlem97  47306  fourierdlem101  47310  fourierdlem103  47312  fourierdlem104  47313  fourierdlem111  47320  fourierdlem112  47321  sqwvfoura  47331  sqwvfourb  47332  fouriersw  47334  elaa2lem  47336  etransclem4  47341  etransclem13  47350  etransclem35  47372  etransclem46  47383  etransclem48  47385  sge0revalmpt  47481  sge0fsummpt  47493  sge0iunmptlemfi  47516  sge0iunmptlemre  47518  sge0ltfirpmpt2  47529  sge0fsummptf  47539  nnfoctbdjlem  47558  iundjiun  47563  meaiunlelem  47571  meaiuninclem  47583  meaiuninc3v  47587  omeiunlempt  47623  carageniuncllem2  47625  caratheodorylem2  47630  0ome  47632  isomenndlem  47633  hoicvr  47651  hoicvrrex  47659  ovn0lem  47668  ovnsubaddlem1  47673  hoidmvlelem2  47699  hoidmvlelem3  47700  ovnhoilem2  47705  hoicoto2  47708  hoi2toco  47710  ovnlecvr2  47713  ovncvr2  47714  ovnsubadd2lem  47748  ovolval5lem2  47756  ovnovollem1  47759  ovnovollem2  47760  vonioolem1  47783  smfaddlem1  47866  smflimlem2  47875  smflimmpt  47913  smflimsuplem2  47924  smflimsuplem4  47926  smflimsuplem5  47927  smflimsupmpt  47932  smfliminfmpt  47935  smfsupdmmbllem  47947  finfdm  47949  smfinfdmmbllem  47951  setrec2mpt  50958  aacllem  51107