Theorem dffunALTV2

Description: Alternate definition of the function relation predicate, cf. dfdisjALTV2 . (Contributed by Peter Mazsa, 8-Feb-2018)

	Ref	Expression
Assertion	dffunALTV2	$$⊢FunALTVF\leftrightarrow \left(\wr F\subseteq \mathrm{I}\wedge \mathrm{Rel}F\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-funALTV	$$⊢FunALTVF\leftrightarrow \left(CnvRefRel\wr F\wedge \mathrm{Rel}F\right)$$
2		cnvrefrelcoss2	$$⊢CnvRefRel\wr F\leftrightarrow \wr F\subseteq \mathrm{I}$$
3	2	anbi1i	$$⊢\left(CnvRefRel\wr F\wedge \mathrm{Rel}F\right)\leftrightarrow \left(\wr F\subseteq \mathrm{I}\wedge \mathrm{Rel}F\right)$$
4	1 3	bitri	$$⊢FunALTVF\leftrightarrow \left(\wr F\subseteq \mathrm{I}\wedge \mathrm{Rel}F\right)$$