![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbfv2g | Structured version Visualization version GIF version |
Description: Move class substitution in and out of a function value. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbfv2g | ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (𝐹‘⦋𝐴 / 𝑥⦌𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbfv12 6967 | . 2 ⊢ ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵) | |
2 | csbconstg 3934 | . . 3 ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌𝐹 = 𝐹) | |
3 | 2 | fveq1d 6921 | . 2 ⊢ (𝐴 ∈ 𝐶 → (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵) = (𝐹‘⦋𝐴 / 𝑥⦌𝐵)) |
4 | 1, 3 | eqtrid 2786 | 1 ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (𝐹‘⦋𝐴 / 𝑥⦌𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2103 ⦋csb 3915 ‘cfv 6572 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2105 ax-9 2113 ax-10 2136 ax-11 2153 ax-12 2173 ax-ext 2705 ax-nul 5327 ax-pr 5450 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2890 df-ral 3064 df-rex 3073 df-rab 3439 df-v 3484 df-sbc 3799 df-csb 3916 df-dif 3973 df-un 3975 df-ss 3987 df-nul 4348 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5170 df-dm 5709 df-iota 6524 df-fv 6580 |
This theorem is referenced by: csbfv 6969 ixpsnval 8954 swrdspsleq 14709 sumeq2ii 15737 fsumabs 15845 prodeq2ii 15955 fprodabs 16016 ixpsnbasval 21233 coe1fzgsumdlem 22321 evl1gsumdlem 22374 pm2mp 22845 cayhamlem4 22908 iuninc 32574 cdlemk39s 40844 evl1gprodd 42022 minregex 43436 |
Copyright terms: Public domain | W3C validator |