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

Metamath Proof Explorer

Theorem csbmpt2

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

Ref Expression
Assertion csbmpt2 ⊢ A ∈ V → ⦋ A / x⦌ y ∈ Y ⟼ Z = y ∈ Y ⟼ ⦋ A / x⦌ Z

Proof

Step Hyp Ref Expression
1 csbmpt12 ⊢ A ∈ V → ⦋ A / x⦌ y ∈ Y ⟼ Z = y ∈ ⦋ A / x⦌ Y ⟼ ⦋ A / x⦌ Z
2 csbconstg ⊢ A ∈ V → ⦋ A / x⦌ Y = Y
3 2 mpteq1d ⊢ A ∈ V → y ∈ ⦋ A / x⦌ Y ⟼ ⦋ A / x⦌ Z = y ∈ Y ⟼ ⦋ A / x⦌ Z
4 1 3 eqtrd ⊢ A ∈ V → ⦋ A / x⦌ y ∈ Y ⟼ Z = y ∈ Y ⟼ ⦋ A / x⦌ Z