Theorem csbfv 6881

Description: Substitution for a function value. (Contributed by NM, 1-Jan-2006.) (Revised by NM, 20-Aug-2018.)

Assertion

Ref	Expression
csbfv	⊢ ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = (𝐹‘𝐴)

Distinct variable group:   𝑥,𝐹

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem csbfv

Step	Hyp	Ref	Expression
1		csbfv2g 6880	. . 3 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = (𝐹‘⦋𝐴 / 𝑥⦌𝑥))
2		csbvarg 4369	. . . 4 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)
3	2	fveq2d 6838	. . 3 ⊢ (𝐴 ∈ V → (𝐹‘⦋𝐴 / 𝑥⦌𝑥) = (𝐹‘𝐴))
4	1, 3	eqtrd 2775	. 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = (𝐹‘𝐴))
5		csbprc 4344	. . 3 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = ∅)
6		fvprc 6826	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
7	5, 6	eqtr4d 2778	. 2 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = (𝐹‘𝐴))
8	4, 7	pm2.61i 183	1 ⊢ ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = (𝐹‘𝐴)

Syntax hints:  ¬ wn 3   = wceq 1547   ∈ wcel 2119  Vcvv 3432  ⦋csb 3838  ∅c0 4268  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-dm 5635  df-iota 6448  df-fv 6500

This theorem is referenced by:  mptcoe1fsupp  22207  mptcoe1matfsupp  22792  mp2pm2mplem4  22799  chfacfscmulfsupp  22849  chfacfpmmulfsupp  22853  cpmidpmatlem3  22862  cayhamlem4  22878  cayleyhamilton1  22882  logbmpt  26777  nbgrcl  29429  nbgrnvtx0  29433  iuninc  32656  disjxpin  32684  finixpnum  37979  cdlemkid3N  41432  cdlemkid4  41433  cdlemk39s  41438  mccllem  46049  clnbgrcl  48319  clnbgrnvtx0  48325