Description: An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | reloprab | |- Rel { <. <. x , y >. , z >. | ph } |
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 } |