Metamath Proof Explorer

Theorem csbima12

Description: Move class substitution in and out of the image of a function. (Contributed by FL, 15-Dec-2006) (Revised by NM, 20-Aug-2018)

Ref Expression
Assertion csbima12 ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )

Proof

Step Hyp Ref Expression
1 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ ( 𝐹 “ 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ 𝐵 ) )
2 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ 𝐹 )
3 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
4 2 3 imaeq12d ⊢ ( 𝑦 = 𝐴 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
5 1 4 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( ⦋ 𝑦 / 𝑥 ⦌ ( 𝐹 “ 𝐵 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
6 vex ⊢ 𝑦 ∈ V
7 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐹
8 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
9 7 8 nfima ⊢ Ⅎ 𝑥 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
10 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐹 = ⦋ 𝑦 / 𝑥 ⦌ 𝐹 )
11 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
12 10 11 imaeq12d ⊢ ( 𝑥 = 𝑦 → ( 𝐹 “ 𝐵 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
13 6 9 12 csbief ⊢ ⦋ 𝑦 / 𝑥 ⦌ ( 𝐹 “ 𝐵 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
14 5 13 vtoclg ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
15 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ 𝐵 ) = ∅ )
16 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ )
17 16 imaeq2d ⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ∅ ) )
18 ima0 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ∅ ) = ∅
19 17 18 eqtr2di ⊢ ( ¬ 𝐴 ∈ V → ∅ = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
20 15 19 eqtrd ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
21 14 20 pm2.61i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )