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 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∣ 𝑓 : 𝑦 ⟶ 𝑥 } )
2	1	reldmmpo	⊢ Rel dom ↑m