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 >. | ph }

Proof

Step Hyp Ref Expression
1 dfoprab2 
 |-  { <. <. x , y >. , z >. | ph } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) }
2 1 relopabiv 
 |-  Rel { <. <. x , y >. , z >. | ph }