Theorem fndmu 3595

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 3593	. 2 |- (F Fn A -> dom F = A)
2		fndm 3593	. 2 |- (F Fn B -> dom F = B)
3	1, 2	sylan9req 1531	1 |- ((F Fn A /\ F Fn B) -> A = B)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 958  dom cdm 3176   Fn wfn 3183

This theorem is referenced by:  fodmrnu 3686  grprn 8053  vcoprnelem 8193  hon0 9714

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1472  df-fn 3199

Copyright terms: Public domain