Theorem csbrecsg

Description: Move class substitution in and out of recs . (Contributed by ML, 25-Oct-2020)

	Ref	Expression
Assertion	csbrecsg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ recs ( 𝐹 ) = recs ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		csbwrecsg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ wrecs ( E , On , 𝐹 ) = wrecs ( ⦋ 𝐴 / 𝑥 ⦌ E , ⦋ 𝐴 / 𝑥 ⦌ On , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )
2		csbconstg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ E = E )
3		wrecseq1	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ E = E → wrecs ( ⦋ 𝐴 / 𝑥 ⦌ E , ⦋ 𝐴 / 𝑥 ⦌ On , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) = wrecs ( E , ⦋ 𝐴 / 𝑥 ⦌ On , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )
4	2 3	syl	⊢ ( 𝐴 ∈ 𝑉 → wrecs ( ⦋ 𝐴 / 𝑥 ⦌ E , ⦋ 𝐴 / 𝑥 ⦌ On , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) = wrecs ( E , ⦋ 𝐴 / 𝑥 ⦌ On , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )
5		csbconstg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ On = On )
6		wrecseq2	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ On = On → wrecs ( E , ⦋ 𝐴 / 𝑥 ⦌ On , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) = wrecs ( E , On , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )
7	5 6	syl	⊢ ( 𝐴 ∈ 𝑉 → wrecs ( E , ⦋ 𝐴 / 𝑥 ⦌ On , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) = wrecs ( E , On , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )
8	1 4 7	3eqtrd	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ wrecs ( E , On , 𝐹 ) = wrecs ( E , On , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )
9		df-recs	⊢ recs ( 𝐹 ) = wrecs ( E , On , 𝐹 )
10	9	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ recs ( 𝐹 ) = ⦋ 𝐴 / 𝑥 ⦌ wrecs ( E , On , 𝐹 )
11		df-recs	⊢ recs ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) = wrecs ( E , On , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 )
12	8 10 11	3eqtr4g	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ recs ( 𝐹 ) = recs ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )