Theorem csbmpt12

Description: Move substitution into a maps-to notation. (Contributed by AV, 26-Sep-2019)

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

Proof

Step	Hyp	Ref	Expression
1		csbopab	$$⊢⦋A/x⦌\left\{⟨y,z⟩|\left(y\in Y\wedge z=Z\right)\right\}=\left\{⟨y,z⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in Y\wedge z=Z\right)\right\}$$
2		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in Y\wedge z=Z\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in Y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=Z\right)$$
3		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in Y\leftrightarrow ⦋A/x⦌y\in ⦋A/x⦌Y$$
4		csbconstg	$$⊢A\in V\to ⦋A/x⦌y=y$$
5	4	eleq1d	$$⊢A\in V\to \left(⦋A/x⦌y\in ⦋A/x⦌Y\leftrightarrow y\in ⦋A/x⦌Y\right)$$
6	3 5	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in Y\leftrightarrow y\in ⦋A/x⦌Y\right)$$
7		sbceq2g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=Z\leftrightarrow z=⦋A/x⦌Z\right)$$
8	6 7	anbi12d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in Y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=Z\right)\leftrightarrow \left(y\in ⦋A/x⦌Y\wedge z=⦋A/x⦌Z\right)\right)$$
9	2 8	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in Y\wedge z=Z\right)\leftrightarrow \left(y\in ⦋A/x⦌Y\wedge z=⦋A/x⦌Z\right)\right)$$
10	9	opabbidv	$$⊢A\in V\to \left\{⟨y,z⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in Y\wedge z=Z\right)\right\}=\left\{⟨y,z⟩|\left(y\in ⦋A/x⦌Y\wedge z=⦋A/x⦌Z\right)\right\}$$
11	1 10	eqtrid	$$⊢A\in V\to ⦋A/x⦌\left\{⟨y,z⟩|\left(y\in Y\wedge z=Z\right)\right\}=\left\{⟨y,z⟩|\left(y\in ⦋A/x⦌Y\wedge z=⦋A/x⦌Z\right)\right\}$$
12		df-mpt	$$⊢\left(y\in Y⟼Z\right)=\left\{⟨y,z⟩|\left(y\in Y\wedge z=Z\right)\right\}$$
13	12	csbeq2i	$$⊢⦋A/x⦌\left(y\in Y⟼Z\right)=⦋A/x⦌\left\{⟨y,z⟩|\left(y\in Y\wedge z=Z\right)\right\}$$
14		df-mpt	$$⊢\left(y\in ⦋A/x⦌Y⟼⦋A/x⦌Z\right)=\left\{⟨y,z⟩|\left(y\in ⦋A/x⦌Y\wedge z=⦋A/x⦌Z\right)\right\}$$
15	11 13 14	3eqtr4g	$$⊢A\in V\to ⦋A/x⦌\left(y\in Y⟼Z\right)=\left(y\in ⦋A/x⦌Y⟼⦋A/x⦌Z\right)$$