Metamath Proof Explorer

Theorem fndmu

Description: A function has a unique domain. (Contributed by NM, 11-Aug-1994)

Ref Expression
Assertion fndmu 
|- ( ( F Fn A /\ F Fn B ) -> A = B )

Proof

Step Hyp Ref Expression
1 fndm 
 |-  ( F Fn A -> dom F = A )
2 fndm 
 |-  ( F Fn B -> dom F = B )
3 1 2 sylan9req 
 |-  ( ( F Fn A /\ F Fn B ) -> A = B )