dffun9

Description: Alternate definition of a function. (Contributed by NM, 28-Mar-2007) (Revised by NM, 16-Jun-2017)

		Ref	Expression
	Assertion	dffun9	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \in dom A \exists^{*} y \in ran A x A y)$

Step	Hyp	Ref	Expression
1		dffun7	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \in dom A \exists^{*} y x A y)$
2		vex	$⊢ x \in V$
3		vex	$⊢ y \in V$
4	2 3	brelrn	$⊢ x A y \to y \in ran A$
5	4	pm4.71ri	$⊢ x A y \leftrightarrow (y \in ran A \land x A y)$
6	5	mobii	$⊢ \exists^{} y x A y \leftrightarrow \exists^{} y (y \in ran A \land x A y)$
7		df-rmo	$⊢ \exists^{} y \in ran A x A y \leftrightarrow \exists^{} y (y \in ran A \land x A y)$
8	6 7	bitr4i	$⊢ \exists^{} y x A y \leftrightarrow \exists^{} y \in ran A x A y$
9	8	ralbii	$⊢ \forall x \in dom A \exists^{} y x A y \leftrightarrow \forall x \in dom A \exists^{} y \in ran A x A y$
10	9	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 \in ran A x A y)$
11	1 10	bitri	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \in dom A \exists^{*} y \in ran A x A y)$

Metamath Proof Explorer