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 ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑦 ∈ 𝑌 ↦ 𝑍 ) = ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ↦ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) )

Proof

Step Hyp Ref Expression
1 csbopab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍 ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍 ) }
2 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑌 ∧ [ 𝐴 / 𝑥 ] 𝑧 = 𝑍 ) )
3 sbcel12 ⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑌 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 )
4 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 )
5 4 eleq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ) )
6 3 5 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑌 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ) )
7 sbceq2g ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 = 𝑍 ↔ 𝑧 = ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) )
8 6 7 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑌 ∧ [ 𝐴 / 𝑥 ] 𝑧 = 𝑍 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 = ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) ) )
9 2 8 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 = ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) ) )
10 9 opabbidv ⊢ ( 𝐴 ∈ 𝑉 → { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍 ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 = ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) } )
11 1 10 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍 ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 = ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) } )
12 df-mpt ⊢ ( 𝑦 ∈ 𝑌 ↦ 𝑍 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍 ) }
13 12 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑦 ∈ 𝑌 ↦ 𝑍 ) = ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝑌 ∧ 𝑧 = 𝑍 ) }
14 df-mpt ⊢ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ↦ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 = ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) }
15 11 13 14 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑦 ∈ 𝑌 ↦ 𝑍 ) = ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ↦ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) )