This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ffn

Description: A mapping is a function with domain. (Contributed by NM, 2-Aug-1994)

Ref Expression
Assertion ffn 
|- ( F : A --> B -> F Fn A )

Proof

Step Hyp Ref Expression
1 df-f 
 |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2 1 simplbi 
 |-  ( F : A --> B -> F Fn A )