funmo

Description: A function has at most one value for each argument. (Contributed by NM, 24-May-1998) (Proof shortened by SN, 19-Dec-2024)

		Ref	Expression
	Assertion	funmo	$⊢ Fun F \to \exists^{*} y A F y$

Step	Hyp	Ref	Expression
1		dffun6	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \exists^{*} y x F y)$
2	1	simplbi	$⊢ Fun F \to Rel F$
3		brrelex1	$⊢ (Rel F \land A F y) \to A \in V$
4	3	ex	$⊢ Rel F \to (A F y \to A \in V)$
5	2 4	syl	$⊢ Fun F \to (A F y \to A \in V)$
6	5	ancrd	$⊢ Fun F \to (A F y \to (A \in V \land A F y))$
7	6	alrimiv	$⊢ Fun F \to \forall y (A F y \to (A \in V \land A F y))$
8	1	simprbi	$⊢ Fun F \to \forall x \exists^{*} y x F y$
9		breq1	$⊢ x = A \to (x F y \leftrightarrow A F y)$
10	9	mobidv	$⊢ x = A \to (\exists^{} y x F y \leftrightarrow \exists^{} y A F y)$
11	10	spcgv	$⊢ A \in V \to (\forall x \exists^{} y x F y \to \exists^{} y A F y)$
12	8 11	syl5com	$⊢ Fun F \to (A \in V \to \exists^{*} y A F y)$
13		moanimv	$⊢ \exists^{} y (A \in V \land A F y) \leftrightarrow (A \in V \to \exists^{} y A F y)$
14	12 13	sylibr	$⊢ Fun F \to \exists^{*} y (A \in V \land A F y)$
15		moim	$⊢ \forall y (A F y \to (A \in V \land A F y)) \to (\exists^{} y (A \in V \land A F y) \to \exists^{} y A F y)$
16	7 14 15	sylc	$⊢ Fun F \to \exists^{*} y A F y$

Metamath Proof Explorer