dffun4

Description: Alternate definition of a function. Definition 6.4(4) of TakeutiZaring p. 24. (Contributed by NM, 29-Dec-1996)

		Ref	Expression
	Assertion	dffun4	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \forall y \forall z ((⟨x, y⟩ \in A \land ⟨x, z⟩ \in A) \to y = z))$

Step	Hyp	Ref	Expression
1		dffun2	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \forall y \forall z ((x A y \land x A z) \to y = z))$
2		df-br	$⊢ x A y \leftrightarrow ⟨x, y⟩ \in A$
3		df-br	$⊢ x A z \leftrightarrow ⟨x, z⟩ \in A$
4	2 3	anbi12i	$⊢ (x A y \land x A z) \leftrightarrow (⟨x, y⟩ \in A \land ⟨x, z⟩ \in A)$
5	4	imbi1i	$⊢ ((x A y \land x A z) \to y = z) \leftrightarrow ((⟨x, y⟩ \in A \land ⟨x, z⟩ \in A) \to y = z)$
6	5	albii	$⊢ \forall z ((x A y \land x A z) \to y = z) \leftrightarrow \forall z ((⟨x, y⟩ \in A \land ⟨x, z⟩ \in A) \to y = z)$
7	6	2albii	$⊢ \forall x \forall y \forall z ((x A y \land x A z) \to y = z) \leftrightarrow \forall x \forall y \forall z ((⟨x, y⟩ \in A \land ⟨x, z⟩ \in A) \to y = z)$
8	7	anbi2i	$⊢ (Rel A \land \forall x \forall y \forall z ((x A y \land x A z) \to y = z)) \leftrightarrow (Rel A \land \forall x \forall y \forall z ((⟨x, y⟩ \in A \land ⟨x, z⟩ \in A) \to y = z))$
9	1 8	bitri	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \forall y \forall z ((⟨x, y⟩ \in A \land ⟨x, z⟩ \in A) \to y = z))$

Metamath Proof Explorer