Metamath Proof Explorer


Theorem opabbi

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

Ref Expression
Assertion opabbi x y φ ψ x y | φ = x y | ψ

Proof

Step Hyp Ref Expression
1 eqopab2b x y | φ = x y | ψ x y φ ψ
2 1 biimpri x y φ ψ x y | φ = x y | ψ