Metamath Proof Explorer

Theorem dffun8

Description: Alternate definition of a function. One possibility for the definition of a function in Enderton p. 42. Compare dffun7 . (Contributed by NM, 4-Nov-2002) (Proof shortened by Andrew Salmon, 17-Sep-2011)

		Ref	Expression
	Assertion	dffun8	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \in dom A \exists! y x A y)$

Proof

Step	Hyp	Ref	Expression
1		dffun7	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \in dom A \exists^{*} y x A y)$
2		moeu	$⊢ \exists^{*} y x A y \leftrightarrow (\exists y x A y \to \exists! y x A y)$
3		vex	$⊢ x \in V$
4	3	eldm	$⊢ x \in dom A \leftrightarrow \exists y x A y$
5		pm5.5	$⊢ \exists y x A y \to ((\exists y x A y \to \exists! y x A y) \leftrightarrow \exists! y x A y)$
6	4 5	sylbi	$⊢ x \in dom A \to ((\exists y x A y \to \exists! y x A y) \leftrightarrow \exists! y x A y)$
7	2 6	bitrid	$⊢ x \in dom A \to (\exists^{*} y x A y \leftrightarrow \exists! y x A y)$
8	7	ralbiia	$⊢ \forall x \in dom A \exists^{*} y x A y \leftrightarrow \forall x \in dom A \exists! y x A y$
9	8	anbi2i	$⊢ (Rel A \land \forall x \in dom A \exists^{*} y x A y) \leftrightarrow (Rel A \land \forall x \in dom A \exists! y x A y)$
10	1 9	bitri	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \in dom A \exists! y x A y)$