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 )