Metamath Proof Explorer

Theorem svrelfun

Description: A single-valued relation is a function. (See fun2cnv for "single-valued.") Definition 6.4(4) of TakeutiZaring p. 24. (Contributed by NM, 17-Jan-2006)

		Ref	Expression
	Assertion	svrelfun	$⊢ Fun A \leftrightarrow (Rel A \land Fun {A^{-1}}^{-1})$

Proof

Step	Hyp	Ref	Expression
1		dffun6	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \exists^{*} y x A y)$
2		fun2cnv	$⊢ Fun {A^{-1}}^{-1} \leftrightarrow \forall x \exists^{*} y x A y$
3	2	anbi2i	$⊢ (Rel A \land Fun {A^{-1}}^{-1}) \leftrightarrow (Rel A \land \forall x \exists^{*} y x A y)$
4	1 3	bitr4i	$⊢ Fun A \leftrightarrow (Rel A \land Fun {A^{-1}}^{-1})$