fununiq

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

Step	Hyp	Ref	Expression
1		fununiq.1	$⊢ A \in V$
2		fununiq.2	$⊢ B \in V$
3		fununiq.3	$⊢ C \in V$
4		dffun2	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \forall y \forall z ((x F y \land x F z) \to y = z))$
5		breq12	$⊢ (x = A \land y = B) \to (x F y \leftrightarrow A F B)$
6	5	3adant3	$⊢ (x = A \land y = B \land z = C) \to (x F y \leftrightarrow A F B)$
7		breq12	$⊢ (x = A \land z = C) \to (x F z \leftrightarrow A F C)$
8	7	3adant2	$⊢ (x = A \land y = B \land z = C) \to (x F z \leftrightarrow A F C)$
9	6 8	anbi12d	$⊢ (x = A \land y = B \land z = C) \to ((x F y \land x F z) \leftrightarrow (A F B \land A F C))$
10		eqeq12	$⊢ (y = B \land z = C) \to (y = z \leftrightarrow B = C)$
11	10	3adant1	$⊢ (x = A \land y = B \land z = C) \to (y = z \leftrightarrow B = C)$
12	9 11	imbi12d	$⊢ (x = A \land y = B \land z = C) \to (((x F y \land x F z) \to y = z) \leftrightarrow ((A F B \land A F C) \to B = C))$
13	12	spc3gv	$⊢ (A \in V \land B \in V \land C \in V) \to (\forall x \forall y \forall z ((x F y \land x F z) \to y = z) \to ((A F B \land A F C) \to B = C))$
14	1 2 3 13	mp3an	$⊢ \forall x \forall y \forall z ((x F y \land x F z) \to y = z) \to ((A F B \land A F C) \to B = C)$
15	4 14	simplbiim	$⊢ Fun F \to ((A F B \land A F C) \to B = C)$

Metamath Proof Explorer