Description: Weak dominance is a relation. (Contributed by Stefan O'Rear, 11-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | relwdom | |- Rel ~<_* |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-wdom | |- ~<_* = { <. x , y >. | ( x = (/) \/ E. z z : y -onto-> x ) } |
|
2 | 1 | relopabi | |- Rel ~<_* |