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 ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )

Proof

Step Hyp Ref Expression
1 csbiota ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝐵 𝐹 𝑦 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝐵 𝐹 𝑦 )
2 sbcbr123 ⊢ ( [ 𝐴 / 𝑥 ] 𝐵 𝐹 𝑦 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝑦 )
3 csbconstg ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 )
4 3 breq2d ⊢ ( 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 ) )
5 2 4 bitrid ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝐵 𝐹 𝑦 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 ) )
6 5 iotabidv ⊢ ( 𝐴 ∈ V → ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝐵 𝐹 𝑦 ) = ( ℩ 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 ) )
7 1 6 eqtrid ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝐵 𝐹 𝑦 ) = ( ℩ 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 ) )
8 df-fv ⊢ ( 𝐹 ‘ 𝐵 ) = ( ℩ 𝑦 𝐵 𝐹 𝑦 )
9 8 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝐵 𝐹 𝑦 )
10 df-fv ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ( ℩ 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 )
11 7 9 10 3eqtr4g ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
12 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ∅ )
13 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ∅ )
14 13 fveq1d ⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ( ∅ ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
15 0fv ⊢ ( ∅ ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ∅
16 14 15 eqtr2di ⊢ ( ¬ 𝐴 ∈ V → ∅ = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
17 12 16 eqtrd ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
18 11 17 pm2.61i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )