Metamath Proof Explorer


Theorem csbafv12g

Description: Move class substitution in and out of a function value, analogous to csbfv12 , with a direct proof proposed by Mario Carneiro, analogous to csbov123 . (Contributed by Alexander van der Vekens, 23-Jul-2017)

Ref Expression
Assertion csbafv12g ( 𝐴𝑉 𝐴 / 𝑥 ( 𝐹 ''' 𝐵 ) = ( 𝐴 / 𝑥 𝐹 ''' 𝐴 / 𝑥 𝐵 ) )

Proof

Step Hyp Ref Expression
1 csbeq1 ( 𝑦 = 𝐴 𝑦 / 𝑥 ( 𝐹 ''' 𝐵 ) = 𝐴 / 𝑥 ( 𝐹 ''' 𝐵 ) )
2 csbeq1 ( 𝑦 = 𝐴 𝑦 / 𝑥 𝐹 = 𝐴 / 𝑥 𝐹 )
3 csbeq1 ( 𝑦 = 𝐴 𝑦 / 𝑥 𝐵 = 𝐴 / 𝑥 𝐵 )
4 2 3 afveq12d ( 𝑦 = 𝐴 → ( 𝑦 / 𝑥 𝐹 ''' 𝑦 / 𝑥 𝐵 ) = ( 𝐴 / 𝑥 𝐹 ''' 𝐴 / 𝑥 𝐵 ) )
5 1 4 eqeq12d ( 𝑦 = 𝐴 → ( 𝑦 / 𝑥 ( 𝐹 ''' 𝐵 ) = ( 𝑦 / 𝑥 𝐹 ''' 𝑦 / 𝑥 𝐵 ) ↔ 𝐴 / 𝑥 ( 𝐹 ''' 𝐵 ) = ( 𝐴 / 𝑥 𝐹 ''' 𝐴 / 𝑥 𝐵 ) ) )
6 vex 𝑦 ∈ V
7 nfcsb1v 𝑥 𝑦 / 𝑥 𝐹
8 nfcsb1v 𝑥 𝑦 / 𝑥 𝐵
9 7 8 nfafv 𝑥 ( 𝑦 / 𝑥 𝐹 ''' 𝑦 / 𝑥 𝐵 )
10 csbeq1a ( 𝑥 = 𝑦𝐹 = 𝑦 / 𝑥 𝐹 )
11 csbeq1a ( 𝑥 = 𝑦𝐵 = 𝑦 / 𝑥 𝐵 )
12 10 11 afveq12d ( 𝑥 = 𝑦 → ( 𝐹 ''' 𝐵 ) = ( 𝑦 / 𝑥 𝐹 ''' 𝑦 / 𝑥 𝐵 ) )
13 6 9 12 csbief 𝑦 / 𝑥 ( 𝐹 ''' 𝐵 ) = ( 𝑦 / 𝑥 𝐹 ''' 𝑦 / 𝑥 𝐵 )
14 5 13 vtoclg ( 𝐴𝑉 𝐴 / 𝑥 ( 𝐹 ''' 𝐵 ) = ( 𝐴 / 𝑥 𝐹 ''' 𝐴 / 𝑥 𝐵 ) )