Metamath Proof Explorer


Theorem reldmoprab

Description: The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995)

Ref Expression
Assertion reldmoprab Rel dom x y z | φ

Proof

Step Hyp Ref Expression
1 dmoprab dom x y z | φ = x y | z φ
2 1 relopabiv Rel dom x y z | φ