Theorem csbopg

Description: Distribution of class substitution over ordered pairs. (Contributed by Drahflow, 25-Sep-2015) (Revised by Mario Carneiro, 29-Oct-2015) (Revised by ML, 25-Oct-2020)

	Ref	Expression
Assertion	csbopg	$$⊢A\in V\to ⦋A/x⦌⟨C,D⟩=⟨⦋A/x⦌C,⦋A/x⦌D⟩$$

Proof

Step	Hyp	Ref	Expression
1		csbif	$$⊢⦋A/x⦌if\left(\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right),\left\{\left\{C\right\},\left\{C,D\right\}\right\},\varnothing \right)=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right),⦋A/x⦌\left\{\left\{C\right\},\left\{C,D\right\}\right\},⦋A/x⦌\varnothing \right)$$
2		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\in \mathrm{V}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}D\in \mathrm{V}\right)$$
3		sbcel1g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\in \mathrm{V}\leftrightarrow ⦋A/x⦌C\in \mathrm{V}\right)$$
4		sbcel1g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}D\in \mathrm{V}\leftrightarrow ⦋A/x⦌D\in \mathrm{V}\right)$$
5	3 4	anbi12d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\in \mathrm{V}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}D\in \mathrm{V}\right)\leftrightarrow \left(⦋A/x⦌C\in \mathrm{V}\wedge ⦋A/x⦌D\in \mathrm{V}\right)\right)$$
6	2 5	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)\leftrightarrow \left(⦋A/x⦌C\in \mathrm{V}\wedge ⦋A/x⦌D\in \mathrm{V}\right)\right)$$
7		csbprg	$$⊢A\in V\to ⦋A/x⦌\left\{\left\{C\right\},\left\{C,D\right\}\right\}=\left\{⦋A/x⦌\left\{C\right\},⦋A/x⦌\left\{C,D\right\}\right\}$$
8		csbsng	$$⊢A\in V\to ⦋A/x⦌\left\{C\right\}=\left\{⦋A/x⦌C\right\}$$
9		csbprg	$$⊢A\in V\to ⦋A/x⦌\left\{C,D\right\}=\left\{⦋A/x⦌C,⦋A/x⦌D\right\}$$
10	8 9	preq12d	$$⊢A\in V\to \left\{⦋A/x⦌\left\{C\right\},⦋A/x⦌\left\{C,D\right\}\right\}=\left\{\left\{⦋A/x⦌C\right\},\left\{⦋A/x⦌C,⦋A/x⦌D\right\}\right\}$$
11	7 10	eqtrd	$$⊢A\in V\to ⦋A/x⦌\left\{\left\{C\right\},\left\{C,D\right\}\right\}=\left\{\left\{⦋A/x⦌C\right\},\left\{⦋A/x⦌C,⦋A/x⦌D\right\}\right\}$$
12		csbconstg	$$⊢A\in V\to ⦋A/x⦌\varnothing =\varnothing$$
13	6 11 12	ifbieq12d	$$⊢A\in V\to if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right),⦋A/x⦌\left\{\left\{C\right\},\left\{C,D\right\}\right\},⦋A/x⦌\varnothing \right)=if\left(\left(⦋A/x⦌C\in \mathrm{V}\wedge ⦋A/x⦌D\in \mathrm{V}\right),\left\{\left\{⦋A/x⦌C\right\},\left\{⦋A/x⦌C,⦋A/x⦌D\right\}\right\},\varnothing \right)$$
14	1 13	eqtrid	$$⊢A\in V\to ⦋A/x⦌if\left(\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right),\left\{\left\{C\right\},\left\{C,D\right\}\right\},\varnothing \right)=if\left(\left(⦋A/x⦌C\in \mathrm{V}\wedge ⦋A/x⦌D\in \mathrm{V}\right),\left\{\left\{⦋A/x⦌C\right\},\left\{⦋A/x⦌C,⦋A/x⦌D\right\}\right\},\varnothing \right)$$
15		dfopif	$$⊢⟨C,D⟩=if\left(\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right),\left\{\left\{C\right\},\left\{C,D\right\}\right\},\varnothing \right)$$
16	15	csbeq2i	$$⊢⦋A/x⦌⟨C,D⟩=⦋A/x⦌if\left(\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right),\left\{\left\{C\right\},\left\{C,D\right\}\right\},\varnothing \right)$$
17		dfopif	$$⊢⟨⦋A/x⦌C,⦋A/x⦌D⟩=if\left(\left(⦋A/x⦌C\in \mathrm{V}\wedge ⦋A/x⦌D\in \mathrm{V}\right),\left\{\left\{⦋A/x⦌C\right\},\left\{⦋A/x⦌C,⦋A/x⦌D\right\}\right\},\varnothing \right)$$
18	14 16 17	3eqtr4g	$$⊢A\in V\to ⦋A/x⦌⟨C,D⟩=⟨⦋A/x⦌C,⦋A/x⦌D⟩$$