Theorem csbfv 6925

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 6924	. . 3 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = (𝐹‘⦋𝐴 / 𝑥⦌𝑥))
2		csbvarg 4392	. . . 4 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)
3	2	fveq2d 6882	. . 3 ⊢ (𝐴 ∈ V → (𝐹‘⦋𝐴 / 𝑥⦌𝑥) = (𝐹‘𝐴))
4	1, 3	eqtrd 2795	. 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = (𝐹‘𝐴))
5		csbprc 4367	. . 3 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = ∅)
6		fvprc 6870	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
7	5, 6	eqtr4d 2798	. 2 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = (𝐹‘𝐴))
8	4, 7	pm2.61i 184	1 ⊢ ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = (𝐹‘𝐴)

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2145  Vcvv 3450  ⦋csb 3847  ∅c0 4279  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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 3740  df-csb 3848  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-dm 5665  df-iota 6489  df-fv 6541

This theorem is used by:  mptcoe1fsupp  22440  mptcoe1matfsupp  23027  mp2pm2mplem4  23034  chfacfscmulfsupp  23084  chfacfpmmulfsupp  23088  cpmidpmatlem3  23097  cayhamlem4  23113  cayleyhamilton1  23117  logbmpt  27025  nbgrcl  29795  nbgrnvtx0  29799  iuninc  33034  disjxpin  33061  finixpnum  38359  cdlemkid3N  41806  cdlemkid4  41807  cdlemk39s  41812  mccllem  46427  clnbgrcl  48737  clnbgrnvtx0  48743  veroquadmodzerod  50817