Metamath Proof Explorer


Theorem opabbi2dv

Description: Deduce equality of a relation and an ordered-pair class abstraction. Compare abbi2dv . (Contributed by NM, 24-Feb-2014)

Ref Expression
Hypotheses opabbi2dv.1 Rel 𝐴
opabbi2dv.3 ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴𝜓 ) )
Assertion opabbi2dv ( 𝜑𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )

Proof

Step Hyp Ref Expression
1 opabbi2dv.1 Rel 𝐴
2 opabbi2dv.3 ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴𝜓 ) )
3 opabid2 ( Rel 𝐴 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } = 𝐴 )
4 1 3 ax-mp { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } = 𝐴
5 2 opabbidv ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
6 4 5 eqtr3id ( 𝜑𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )