Metamath Proof Explorer

Theorem f1dmOLD

Description: Obsolete version of f1dm as of 29-May-2024. (Contributed by NM, 8-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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