Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 csboprabg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑑 = 𝐷 ) } = { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ [ 𝐴 / 𝑥 ] ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑑 = 𝐷 ) } )
2 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑑 = 𝐷 ) ↔ ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ [ 𝐴 / 𝑥 ] 𝑑 = 𝐷 ) )
3 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑌 ∧ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑍 ) )
4 sbcel12 ⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑌 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 )
5 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 )
6 5 eleq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ) )
7 4 6 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑌 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ) )
8 sbcel12 ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑍 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 )
9 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑧 = 𝑧 )
10 9 eleq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ↔ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) )
11 8 10 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑍 ↔ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) )
12 7 11 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑌 ∧ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑍 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) ) )
13 3 12 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) ) )
14 sbceq2g ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑑 = 𝐷 ↔ 𝑑 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )
15 13 14 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ [ 𝐴 / 𝑥 ] 𝑑 = 𝐷 ) ↔ ( ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) ∧ 𝑑 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) )
16 2 15 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑑 = 𝐷 ) ↔ ( ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) ∧ 𝑑 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) )
17 16 oprabbidv ⊢ ( 𝐴 ∈ 𝑉 → { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ [ 𝐴 / 𝑥 ] ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑑 = 𝐷 ) } = { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ ( ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) ∧ 𝑑 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } )
18 1 17 eqtrd ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑑 = 𝐷 ) } = { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ ( ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) ∧ 𝑑 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } )
19 df-mpo ⊢ ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐷 ) = { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑑 = 𝐷 ) }
20 19 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐷 ) = ⦋ 𝐴 / 𝑥 ⦌ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ 𝑑 = 𝐷 ) }
21 df-mpo ⊢ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 , 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ↦ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) = { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ ( ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ) ∧ 𝑑 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) }
22 18 20 21 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐷 ) = ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑌 , 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑍 ↦ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )