Theorem mptrel

Description: The maps-to notation always describes a binary relation. (Contributed by Scott Fenton, 16-Apr-2012)

	Ref	Expression
Assertion	mptrel	$$⊢\mathrm{Rel}\left(x\in A⟼B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-mpt	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}\left(x\in A⟼B\right)$$