Theorem csbidm

Description: Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008) (Revised by NM, 18-Aug-2018)

	Ref	Expression
Assertion	csbidm	$$⊢⦋A/x⦌⦋A/x⦌B=⦋A/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		csbnest1g	$$⊢A\in \mathrm{V}\to ⦋A/x⦌⦋A/x⦌B=⦋⦋A/x⦌A/x⦌B$$
2		csbconstg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌A=A$$
3	2	csbeq1d	$$⊢A\in \mathrm{V}\to ⦋⦋A/x⦌A/x⦌B=⦋A/x⦌B$$
4	1 3	eqtrd	$$⊢A\in \mathrm{V}\to ⦋A/x⦌⦋A/x⦌B=⦋A/x⦌B$$
5		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌⦋A/x⦌B=\varnothing$$
6		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B=\varnothing$$
7	5 6	eqtr4d	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌⦋A/x⦌B=⦋A/x⦌B$$
8	4 7	pm2.61i	$$⊢⦋A/x⦌⦋A/x⦌B=⦋A/x⦌B$$