Metamath Proof Explorer


Theorem mptrel

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

Ref Expression
Assertion mptrel Rel ( 𝑥𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 df-mpt ( 𝑥𝐴𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = 𝐵 ) }
2 1 relopabiv Rel ( 𝑥𝐴𝐵 )