Theorem csbmpo123

Description: Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020)

	Ref	Expression
Assertion	csbmpo123	$$⊢A\in V\to ⦋A/x⦌\left(y\in Y,z\in Z⟼D\right)=\left(y\in ⦋A/x⦌Y,z\in ⦋A/x⦌Z⟼⦋A/x⦌D\right)$$

Proof

Step	Hyp	Ref	Expression
1		csboprabg	$$⊢A\in V\to ⦋A/x⦌\left\{⟨⟨y,z⟩,d⟩|\left(\left(y\in Y\wedge z\in Z\right)\wedge d=D\right)\right\}=\left\{⟨⟨y,z⟩,d⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(y\in Y\wedge z\in Z\right)\wedge d=D\right)\right\}$$
2		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(y\in Y\wedge z\in Z\right)\wedge d=D\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in Y\wedge z\in Z\right)\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}d=D\right)$$
3		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in Y\wedge z\in Z\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in Y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in Z\right)$$
4		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in Y\leftrightarrow ⦋A/x⦌y\in ⦋A/x⦌Y$$
5		csbconstg	$$⊢A\in V\to ⦋A/x⦌y=y$$
6	5	eleq1d	$$⊢A\in V\to \left(⦋A/x⦌y\in ⦋A/x⦌Y\leftrightarrow y\in ⦋A/x⦌Y\right)$$
7	4 6	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in Y\leftrightarrow y\in ⦋A/x⦌Y\right)$$
8		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in Z\leftrightarrow ⦋A/x⦌z\in ⦋A/x⦌Z$$
9		csbconstg	$$⊢A\in V\to ⦋A/x⦌z=z$$
10	9	eleq1d	$$⊢A\in V\to \left(⦋A/x⦌z\in ⦋A/x⦌Z\leftrightarrow z\in ⦋A/x⦌Z\right)$$
11	8 10	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in Z\leftrightarrow z\in ⦋A/x⦌Z\right)$$
12	7 11	anbi12d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in Y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in Z\right)\leftrightarrow \left(y\in ⦋A/x⦌Y\wedge z\in ⦋A/x⦌Z\right)\right)$$
13	3 12	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in Y\wedge z\in Z\right)\leftrightarrow \left(y\in ⦋A/x⦌Y\wedge z\in ⦋A/x⦌Z\right)\right)$$
14		sbceq2g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}d=D\leftrightarrow d=⦋A/x⦌D\right)$$
15	13 14	anbi12d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in Y\wedge z\in Z\right)\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}d=D\right)\leftrightarrow \left(\left(y\in ⦋A/x⦌Y\wedge z\in ⦋A/x⦌Z\right)\wedge d=⦋A/x⦌D\right)\right)$$
16	2 15	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(y\in Y\wedge z\in Z\right)\wedge d=D\right)\leftrightarrow \left(\left(y\in ⦋A/x⦌Y\wedge z\in ⦋A/x⦌Z\right)\wedge d=⦋A/x⦌D\right)\right)$$
17	16	oprabbidv	$$⊢A\in V\to \left\{⟨⟨y,z⟩,d⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(y\in Y\wedge z\in Z\right)\wedge d=D\right)\right\}=\left\{⟨⟨y,z⟩,d⟩|\left(\left(y\in ⦋A/x⦌Y\wedge z\in ⦋A/x⦌Z\right)\wedge d=⦋A/x⦌D\right)\right\}$$
18	1 17	eqtrd	$$⊢A\in V\to ⦋A/x⦌\left\{⟨⟨y,z⟩,d⟩|\left(\left(y\in Y\wedge z\in Z\right)\wedge d=D\right)\right\}=\left\{⟨⟨y,z⟩,d⟩|\left(\left(y\in ⦋A/x⦌Y\wedge z\in ⦋A/x⦌Z\right)\wedge d=⦋A/x⦌D\right)\right\}$$
19		df-mpo	$$⊢\left(y\in Y,z\in Z⟼D\right)=\left\{⟨⟨y,z⟩,d⟩|\left(\left(y\in Y\wedge z\in Z\right)\wedge d=D\right)\right\}$$
20	19	csbeq2i	$$⊢⦋A/x⦌\left(y\in Y,z\in Z⟼D\right)=⦋A/x⦌\left\{⟨⟨y,z⟩,d⟩|\left(\left(y\in Y\wedge z\in Z\right)\wedge d=D\right)\right\}$$
21		df-mpo	$$⊢\left(y\in ⦋A/x⦌Y,z\in ⦋A/x⦌Z⟼⦋A/x⦌D\right)=\left\{⟨⟨y,z⟩,d⟩|\left(\left(y\in ⦋A/x⦌Y\wedge z\in ⦋A/x⦌Z\right)\wedge d=⦋A/x⦌D\right)\right\}$$
22	18 20 21	3eqtr4g	$$⊢A\in V\to ⦋A/x⦌\left(y\in Y,z\in Z⟼D\right)=\left(y\in ⦋A/x⦌Y,z\in ⦋A/x⦌Z⟼⦋A/x⦌D\right)$$