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