Metamath Proof Explorer


Theorem reloprab

Description: An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004)

Ref Expression
Assertion reloprab Rel x y z | φ

Proof

Step Hyp Ref Expression
1 dfoprab2 x y z | φ = w z | x y w = x y φ
2 1 relopabiv Rel x y z | φ