Theorem fvmpt2 5615

Description: Value of a function given by the maps-to notation. (Contributed by FL, 21-Jun-2010.)

Hypothesis

Ref	Expression
fvmpt2.1	|- F = ( x e. A |-> B )

Assertion

Ref	Expression
fvmpt2	|- ( ( x e. A /\ B e. C ) -> ( F ` x ) = B )

Distinct variable group:   x, A

Allowed substitution hints:   B( x)   C( x)   F( x)

Proof of Theorem fvmpt2

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		csbeq1 3075	. . 3 |- ( y = x -> [_ y / x ]_ B = [_ x / x ]_ B )
2		csbid 3080	. . 3 |- [_ x / x ]_ B = B
3	1, 2	eqtrdi 2238	. 2 |- ( y = x -> [_ y / x ]_ B = B )
4		fvmpt2.1	. . 3 |- F = ( x e. A |-> B )
5		nfcv 2332	. . . 4 |- F/_ y B
6		nfcsb1v 3105	. . . 4 |- F/_ x [_ y / x ]_ B
7		csbeq1a 3081	. . . 4 |- ( x = y -> B = [_ y / x ]_ B )
8	5, 6, 7	cbvmpt 4113	. . 3 |- ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B )
9	4, 8	eqtri 2210	. 2 |- F = ( y e. A |-> [_ y / x ]_ B )
10	3, 9	fvmptg 5608	1 |- ( ( x e. A /\ B e. C ) -> ( F ` x ) = B )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1364   e. wcel 2160   [_csb 3072   |-> cmpt 4079   ` cfv 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-sbc 2978  df-csb 3073  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4308  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-iota 5193  df-fun 5233  df-fv 5239

This theorem is referenced by:  fvmptssdm  5616  fvmpt2d  5618  fvmptdf  5619  mpteqb  5622  fvmptt  5623  fvmptf  5624  fnmptfvd  5636  ralrnmpt  5674  rexrnmpt  5675  fmptco  5698  f1mpt  5788  offval2  6116  ofrfval2  6117  mptelixpg  6752  dom2lem  6790  mapxpen  6866  xpmapenlem  6867  mkvprop  7174  cc2lem  7283  cc3  7285  fsum3cvg  11404  summodclem2a  11407  fsumf1o  11416  fsum3cvg2  11420  fsumadd  11432  isummulc2  11452  fproddccvg  11598  fprodf1o  11614  txcnp  14168  cnmpt11  14180  cnmpt1t  14182  lgseisenlem2  14848