Metamath Proof Explorer


Theorem oprabbi

Description: Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018)

Ref Expression
Assertion oprabbi ( ∀ 𝑥𝑦𝑧 ( 𝜑𝜓 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } )

Proof

Step Hyp Ref Expression
1 eqoprab2b ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥𝑦𝑧 ( 𝜑𝜓 ) )
2 1 biimpri ( ∀ 𝑥𝑦𝑧 ( 𝜑𝜓 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } )