Theorem csboprabg

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

	Ref	Expression
Assertion	csboprabg	$$⊢A\in V\to ⦋A/x⦌\left\{⟨⟨y,z⟩,d⟩|\phi \right\}=\left\{⟨⟨y,z⟩,d⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		csbab	$$⊢⦋A/x⦌\left\{c|\exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\right\}=\left\{c|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\right\}$$
2		sbcex2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)$$
3		sbcex2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\leftrightarrow \exists z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)$$
4		sbcex2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\leftrightarrow \exists d\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)$$
5		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
6		sbcg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}c=⟨⟨y,z⟩,d⟩\leftrightarrow c=⟨⟨y,z⟩,d⟩\right)$$
7	6	anbi1d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
8	5 7	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\leftrightarrow \left(c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
9	8	exbidv	$$⊢A\in V\to \left(\exists d\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\leftrightarrow \exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
10	4 9	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\leftrightarrow \exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
11	10	exbidv	$$⊢A\in V\to \left(\exists z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\leftrightarrow \exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
12	3 11	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\leftrightarrow \exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
13	12	exbidv	$$⊢A\in V\to \left(\exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\leftrightarrow \exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
14	2 13	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\leftrightarrow \exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
15	14	abbidv	$$⊢A\in V\to \left\{c|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\right\}=\left\{c|\exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right\}$$
16	1 15	eqtrid	$$⊢A\in V\to ⦋A/x⦌\left\{c|\exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\right\}=\left\{c|\exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right\}$$
17		df-oprab	$$⊢\left\{⟨⟨y,z⟩,d⟩|\phi \right\}=\left\{c|\exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\right\}$$
18	17	csbeq2i	$$⊢⦋A/x⦌\left\{⟨⟨y,z⟩,d⟩|\phi \right\}=⦋A/x⦌\left\{c|\exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \phi \right)\right\}$$
19		df-oprab	$$⊢\left\{⟨⟨y,z⟩,d⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}=\left\{c|\exists y\exists z\exists d\left(c=⟨⟨y,z⟩,d⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right\}$$
20	16 18 19	3eqtr4g	$$⊢A\in V\to ⦋A/x⦌\left\{⟨⟨y,z⟩,d⟩|\phi \right\}=\left\{⟨⟨y,z⟩,d⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}$$