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 syl5bb ( 𝐴 ∈ 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 𝐴 / 𝑥 ( 𝐹𝐵 ) = ( 𝐴 / 𝑥 𝐹 𝐴 / 𝑥 𝐵 )