Theorem csbrecsg

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

	Ref	Expression
Assertion	csbrecsg	$$⊢A\in V\to ⦋A/x⦌\mathrm{recs}\left(F\right)=\mathrm{recs}\left(⦋A/x⦌F\right)$$

Proof

Step	Hyp	Ref	Expression
1		csbwrecsg	$$⊢A\in V\to ⦋A/x⦌\mathrm{wrecs}\left(\mathrm{E},\mathrm{On},F\right)=\mathrm{wrecs}\left(⦋A/x⦌\mathrm{E},⦋A/x⦌\mathrm{On},⦋A/x⦌F\right)$$
2		csbconstg	$$⊢A\in V\to ⦋A/x⦌\mathrm{E}=\mathrm{E}$$
3		wrecseq1	$$⊢⦋A/x⦌\mathrm{E}=\mathrm{E}\to \mathrm{wrecs}\left(⦋A/x⦌\mathrm{E},⦋A/x⦌\mathrm{On},⦋A/x⦌F\right)=\mathrm{wrecs}\left(\mathrm{E},⦋A/x⦌\mathrm{On},⦋A/x⦌F\right)$$
4	2 3	syl	$$⊢A\in V\to \mathrm{wrecs}\left(⦋A/x⦌\mathrm{E},⦋A/x⦌\mathrm{On},⦋A/x⦌F\right)=\mathrm{wrecs}\left(\mathrm{E},⦋A/x⦌\mathrm{On},⦋A/x⦌F\right)$$
5		csbconstg	$$⊢A\in V\to ⦋A/x⦌\mathrm{On}=\mathrm{On}$$
6		wrecseq2	$$⊢⦋A/x⦌\mathrm{On}=\mathrm{On}\to \mathrm{wrecs}\left(\mathrm{E},⦋A/x⦌\mathrm{On},⦋A/x⦌F\right)=\mathrm{wrecs}\left(\mathrm{E},\mathrm{On},⦋A/x⦌F\right)$$
7	5 6	syl	$$⊢A\in V\to \mathrm{wrecs}\left(\mathrm{E},⦋A/x⦌\mathrm{On},⦋A/x⦌F\right)=\mathrm{wrecs}\left(\mathrm{E},\mathrm{On},⦋A/x⦌F\right)$$
8	1 4 7	3eqtrd	$$⊢A\in V\to ⦋A/x⦌\mathrm{wrecs}\left(\mathrm{E},\mathrm{On},F\right)=\mathrm{wrecs}\left(\mathrm{E},\mathrm{On},⦋A/x⦌F\right)$$
9		df-recs	$$⊢\mathrm{recs}\left(F\right)=\mathrm{wrecs}\left(\mathrm{E},\mathrm{On},F\right)$$
10	9	csbeq2i	$$⊢⦋A/x⦌\mathrm{recs}\left(F\right)=⦋A/x⦌\mathrm{wrecs}\left(\mathrm{E},\mathrm{On},F\right)$$
11		df-recs	$$⊢\mathrm{recs}\left(⦋A/x⦌F\right)=\mathrm{wrecs}\left(\mathrm{E},\mathrm{On},⦋A/x⦌F\right)$$
12	8 10 11	3eqtr4g	$$⊢A\in V\to ⦋A/x⦌\mathrm{recs}\left(F\right)=\mathrm{recs}\left(⦋A/x⦌F\right)$$