This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⦌ (y \in Y ⟼ Z) = (y \in ⦋ A / x ⦌ Y ⟼ ⦋ A / x ⦌ Z)$

Proof

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