Theorem csbprg

Description: Distribute proper substitution through a pair of classes. (Contributed by Alexander van der Vekens, 4-Sep-2018)

	Ref	Expression
Assertion	csbprg	$$⊢C\in V\to ⦋C/x⦌\left\{A,B\right\}=\left\{⦋C/x⦌A,⦋C/x⦌B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		csbun	$$⊢⦋C/x⦌\left(\left\{A\right\}\cup \left\{B\right\}\right)=⦋C/x⦌\left\{A\right\}\cup ⦋C/x⦌\left\{B\right\}$$
2		csbsng	$$⊢C\in V\to ⦋C/x⦌\left\{A\right\}=\left\{⦋C/x⦌A\right\}$$
3		csbsng	$$⊢C\in V\to ⦋C/x⦌\left\{B\right\}=\left\{⦋C/x⦌B\right\}$$
4	2 3	uneq12d	$$⊢C\in V\to ⦋C/x⦌\left\{A\right\}\cup ⦋C/x⦌\left\{B\right\}=\left\{⦋C/x⦌A\right\}\cup \left\{⦋C/x⦌B\right\}$$
5	1 4	eqtrid	$$⊢C\in V\to ⦋C/x⦌\left(\left\{A\right\}\cup \left\{B\right\}\right)=\left\{⦋C/x⦌A\right\}\cup \left\{⦋C/x⦌B\right\}$$
6		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
7	6	csbeq2i	$$⊢⦋C/x⦌\left\{A,B\right\}=⦋C/x⦌\left(\left\{A\right\}\cup \left\{B\right\}\right)$$
8		df-pr	$$⊢\left\{⦋C/x⦌A,⦋C/x⦌B\right\}=\left\{⦋C/x⦌A\right\}\cup \left\{⦋C/x⦌B\right\}$$
9	5 7 8	3eqtr4g	$$⊢C\in V\to ⦋C/x⦌\left\{A,B\right\}=\left\{⦋C/x⦌A,⦋C/x⦌B\right\}$$