Metamath Proof Explorer

Theorem dffunALTV4

Description: Alternate definition of the function relation predicate, cf. dfdisjALTV4 . This is dffun6 . For the X axis and the Y axis you can convert the right side to ( A. x1 E* y1 x1 F y1 /\ Rel F ) . (Contributed by NM, 9-Mar-1995)

		Ref	Expression
	Assertion	dffunALTV4	$⊢ FunALTV F \leftrightarrow (\forall u \exists^{*} x u F x \land Rel F)$

Proof

Step	Hyp	Ref	Expression
1		dffunALTV2	$⊢ FunALTV F \leftrightarrow (≀ F \subseteq I \land Rel F)$
2		cossssid4	$⊢ ≀ F \subseteq I \leftrightarrow \forall u \exists^{*} x u F x$
3	2	anbi1i	$⊢ (≀ F \subseteq I \land Rel F) \leftrightarrow (\forall u \exists^{*} x u F x \land Rel F)$
4	1 3	bitri	$⊢ FunALTV F \leftrightarrow (\forall u \exists^{*} x u F x \land Rel F)$