Metamath Proof Explorer

Theorem reldmmap

Description: Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015)

Ref Expression
Assertion reldmmap 
|- Rel dom ^m

Proof

Step Hyp Ref Expression
1 df-map 
 |-  ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
2 1 reldmmpo 
 |-  Rel dom ^m