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 A
opabbi2dv.3 φ x y A ψ
Assertion opabbi2dv φ A = x y | ψ

Proof

Step Hyp Ref Expression
1 opabbi2dv.1 Rel A
2 opabbi2dv.3 φ x y A ψ
3 opabid2 Rel A x y | x y A = A
4 1 3 ax-mp x y | x y A = A
5 2 opabbidv φ x y | x y A = x y | ψ
6 4 5 eqtr3id φ A = x y | ψ