This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbfv12

Description: Move class substitution in and out of a function value. (Contributed by NM, 11-Nov-2005) (Revised by NM, 20-Aug-2018)

Ref Expression
Assertion csbfv12 ⊢ ⦋ A / x⦌ F ⁡ B = ⦋ A / x⦌ F ⁡ ⦋ A / x⦌ B

Proof

Step Hyp Ref Expression
1 csbiota ⊢ ⦋ A / x⦌ ι y | B F y = ι y | [˙A / x]˙ B F y
2 sbcbr123 ⊢ [˙A / x]˙ B F y ↔ ⦋ A / x⦌ B ⦋ A / x⦌ F ⦋ A / x⦌ y
3 csbconstg ⊢ A ∈ V → ⦋ A / x⦌ y = y
4 3 breq2d ⊢ A ∈ V → ⦋ A / x⦌ B ⦋ A / x⦌ F ⦋ A / x⦌ y ↔ ⦋ A / x⦌ B ⦋ A / x⦌ F y
5 2 4 bitrid ⊢ A ∈ V → [˙A / x]˙ B F y ↔ ⦋ A / x⦌ B ⦋ A / x⦌ F y
6 5 iotabidv ⊢ A ∈ V → ι y | [˙A / x]˙ B F y = ι y | ⦋ A / x⦌ B ⦋ A / x⦌ F y
7 1 6 eqtrid ⊢ A ∈ V → ⦋ A / x⦌ ι y | B F y = ι y | ⦋ A / x⦌ B ⦋ A / x⦌ F y
8 df-fv ⊢ F ⁡ B = ι y | B F y
9 8 csbeq2i ⊢ ⦋ A / x⦌ F ⁡ B = ⦋ A / x⦌ ι y | B F y
10 df-fv ⊢ ⦋ A / x⦌ F ⁡ ⦋ A / x⦌ B = ι y | ⦋ A / x⦌ B ⦋ A / x⦌ F y
11 7 9 10 3eqtr4g ⊢ A ∈ V → ⦋ A / x⦌ F ⁡ B = ⦋ A / x⦌ F ⁡ ⦋ A / x⦌ B
12 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ F ⁡ B = ∅
13 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ F = ∅
14 13 fveq1d ⊢ ¬ A ∈ V → ⦋ A / x⦌ F ⁡ ⦋ A / x⦌ B = ∅ ⁡ ⦋ A / x⦌ B
15 0fv ⊢ ∅ ⁡ ⦋ A / x⦌ B = ∅
16 14 15 eqtr2di ⊢ ¬ A ∈ V → ∅ = ⦋ A / x⦌ F ⁡ ⦋ A / x⦌ B
17 12 16 eqtrd ⊢ ¬ A ∈ V → ⦋ A / x⦌ F ⁡ B = ⦋ A / x⦌ F ⁡ ⦋ A / x⦌ B
18 11 17 pm2.61i ⊢ ⦋ A / x⦌ F ⁡ B = ⦋ A / x⦌ F ⁡ ⦋ A / x⦌ B