Metamath Proof Explorer

Theorem f1dm

Description: The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014) (Proof shortened by Wolf Lammen, 29-May-2024)

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

Proof

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