Metamath Proof Explorer


Theorem elmapi

Description: A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion elmapi A B C A : C B

Proof

Step Hyp Ref Expression
1 elmapex A B C B V C V
2 elmapg B V C V A B C A : C B
3 1 2 syl A B C A B C A : C B
4 3 ibi A B C A : C B