Metamath Proof Explorer

Theorem csboprabg

Description: Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020)

Ref Expression
Assertion csboprabg ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } )

Proof

Step Hyp Ref Expression
1 csbab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) } = { 𝑐 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) }
2 sbcex2 ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) )
3 sbcex2 ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 [ 𝐴 / 𝑥 ] ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) )
4 sbcex2 ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑑 [ 𝐴 / 𝑥 ] ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) )
5 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
6 sbcg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ↔ 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ) )
7 6 anbi1d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
8 5 7 syl5bb ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
9 8 exbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑑 [ 𝐴 / 𝑥 ] ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
10 4 9 syl5bb ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
11 10 exbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑧 [ 𝐴 / 𝑥 ] ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
12 3 11 syl5bb ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
13 12 exbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
14 2 13 syl5bb ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
15 14 abbidv ⊢ ( 𝐴 ∈ 𝑉 → { 𝑐 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) } = { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) } )
16 1 15 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) } = { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) } )
17 df-oprab ⊢ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ 𝜑 } = { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) }
18 17 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ 𝜑 } = ⦋ 𝐴 / 𝑥 ⦌ { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ 𝜑 ) }
19 df-oprab ⊢ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } = { 𝑐 ∣ ∃ 𝑦 ∃ 𝑧 ∃ 𝑑 ( 𝑐 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∧ [ 𝐴 / 𝑥 ] 𝜑 ) }
20 16 18 19 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑑 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } )