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 ( x e. A |-> B )

Proof

Step Hyp Ref Expression
1 df-mpt
 |-  ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
2 1 relopabiv
 |-  Rel ( x e. A |-> B )