MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmpts Structured version   Unicode version

Theorem fvmpts 5973
Description: Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypothesis
Ref Expression
fvmpts.1  |-  F  =  ( x  e.  C  |->  B )
Assertion
Ref Expression
fvmpts  |-  ( ( A  e.  C  /\  [_ A  /  x ]_ B  e.  V )  ->  ( F `  A
)  =  [_ A  /  x ]_ B )
Distinct variable group:    x, C
Allowed substitution hints:    A( x)    B( x)    F( x)    V( x)

Proof of Theorem fvmpts
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 csbeq1 3404 . 2  |-  ( y  =  A  ->  [_ y  /  x ]_ B  = 
[_ A  /  x ]_ B )
2 fvmpts.1 . . 3  |-  F  =  ( x  e.  C  |->  B )
3 nfcv 2585 . . . 4  |-  F/_ y B
4 nfcsb1v 3417 . . . 4  |-  F/_ x [_ y  /  x ]_ B
5 csbeq1a 3410 . . . 4  |-  ( x  =  y  ->  B  =  [_ y  /  x ]_ B )
63, 4, 5cbvmpt 4521 . . 3  |-  ( x  e.  C  |->  B )  =  ( y  e.  C  |->  [_ y  /  x ]_ B )
72, 6eqtri 2452 . 2  |-  F  =  ( y  e.  C  |-> 
[_ y  /  x ]_ B )
81, 7fvmptg 5968 1  |-  ( ( A  e.  C  /\  [_ A  /  x ]_ B  e.  V )  ->  ( F `  A
)  =  [_ A  /  x ]_ B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1438    e. wcel 1873   [_csb 3401    |-> cmpt 4488   ` cfv 5607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-9 1877  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-sep 4552  ax-nul 4561  ax-pr 4666
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3087  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3918  df-sn 4005  df-pr 4007  df-op 4011  df-uni 4226  df-br 4430  df-opab 4489  df-mpt 4490  df-id 4774  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-iota 5571  df-fun 5609  df-fv 5615
This theorem is referenced by:  fvmptd  5976  fvmpt2curryd  7035  mptnn0fsupp  12221  mptnn0fsuppr  12223  zsum  13789  prodss  14006  fprodser  14008  fprodn0  14038  fprodefsum  14154  pcmpt  14842  issubc  15745  gsummptnn0fz  17620  mptscmfsupp0  18158  gsummoncoe1  18903  fvmptnn04if  19877  prdsdsf  21386  itgparts  23003  dchrisumlema  24330  abfmpeld  28261  abfmpel  28262  cdlemk40  34459  aomclem6  35893  ellimcabssub0  37643  constlimc  37650
  Copyright terms: Public domain W3C validator