Description: Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | reldmmap | |- Rel dom ^m |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-map | |- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } ) |
|
2 | 1 | reldmmpo | |- Rel dom ^m |