Theorem fununiq

Description: The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013)

	Ref	Expression
Hypotheses	fununiq.1	|- A e. _V
	fununiq.2	|- B e. _V
	fununiq.3	|- C e. _V
Assertion	fununiq	|- ( Fun F -> ( ( A F B /\ A F C ) -> B = C ) )

Proof

Step	Hyp	Ref	Expression
1		fununiq.1	|- A e. _V
2		fununiq.2	|- B e. _V
3		fununiq.3	|- C e. _V
4		dffun2	|- ( Fun F <-> ( Rel F /\ A. x A. y A. z ( ( x F y /\ x F z ) -> y = z ) ) )
5		breq12	|- ( ( x = A /\ y = B ) -> ( x F y <-> A F B ) )
6	5	3adant3	|- ( ( x = A /\ y = B /\ z = C ) -> ( x F y <-> A F B ) )
7		breq12	|- ( ( x = A /\ z = C ) -> ( x F z <-> A F C ) )
8	7	3adant2	|- ( ( x = A /\ y = B /\ z = C ) -> ( x F z <-> A F C ) )
9	6 8	anbi12d	|- ( ( x = A /\ y = B /\ z = C ) -> ( ( x F y /\ x F z ) <-> ( A F B /\ A F C ) ) )
10		eqeq12	|- ( ( y = B /\ z = C ) -> ( y = z <-> B = C ) )
11	10	3adant1	|- ( ( x = A /\ y = B /\ z = C ) -> ( y = z <-> B = C ) )
12	9 11	imbi12d	|- ( ( x = A /\ y = B /\ z = C ) -> ( ( ( x F y /\ x F z ) -> y = z ) <-> ( ( A F B /\ A F C ) -> B = C ) ) )
13	12	spc3gv	|- ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( A. x A. y A. z ( ( x F y /\ x F z ) -> y = z ) -> ( ( A F B /\ A F C ) -> B = C ) ) )
14	1 2 3 13	mp3an	|- ( A. x A. y A. z ( ( x F y /\ x F z ) -> y = z ) -> ( ( A F B /\ A F C ) -> B = C ) )
15	4 14	simplbiim	|- ( Fun F -> ( ( A F B /\ A F C ) -> B = C ) )