Theorem reldmmap

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

	Ref	Expression
Assertion	reldmmap	$$⊢\mathrm{Rel}\mathrm{dom}{\uparrow }_{𝑚}$$

Proof

Step	Hyp	Ref	Expression
1		df-map	$$⊢{\uparrow }_{𝑚}=\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left\{f|f:y⟶x\right\}\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}{\uparrow }_{𝑚}$$