Theorem fndmu 2725

Description: A function has a unique domain.

Assertion

Ref	Expression
fndmu	⊢ ((F Fn A ∧ F Fn B) → A = B)

Proof of Theorem fndmu

Step	Hyp	Ref	Expression
1		fndm 2723	. . 3 ⊢ (F Fn A → dom F = A)
2	1	cleqcomd 1106	. 2 ⊢ (F Fn A → A = dom F)
3		fndm 2723	. 2 ⊢ (F Fn B → dom F = B)
4	2, 3	sylan9eq 1144	1 ⊢ ((F Fn A ∧ F Fn B) → A = B)

Syntax hints:   → wi 2   ∧ wa 196   = wceq 1091  dom cdm 2410   Fn wfn 2417

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097  df-fn 2433

metamath.org