Metamath Proof Explorer

Theorem fdmOLD

Description: Obsolete version of fdm as of 29-May-2024. (Contributed by NM, 2-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fdmOLD 
|- ( F : A --> B -> dom F = A )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : A --> B -> F Fn A )
2 fndm 
 |-  ( F Fn A -> dom F = A )
3 1 2 syl 
 |-  ( F : A --> B -> dom F = A )