Theorem fndmu

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

	Ref	Expression
Assertion	fndmu	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐵 ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
2		fndm	⊢ ( 𝐹 Fn 𝐵 → dom 𝐹 = 𝐵 )
3	1 2	sylan9req	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐵 ) → 𝐴 = 𝐵 )