Theorem dffunsALTV

Description: Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021)

	Ref	Expression
Assertion	dffunsALTV	$$⊢\mathrm{FunsALTV}=\left\{f\in \mathrm{Rels}|\wr f\in \mathrm{CnvRefRels}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-funsALTV	$$⊢\mathrm{FunsALTV}=\mathrm{Funss}\cap \mathrm{Rels}$$
2		df-funss	$$⊢\mathrm{Funss}=\left\{f|\wr f\in \mathrm{CnvRefRels}\right\}$$
3	1 2	abeqin	$$⊢\mathrm{FunsALTV}=\left\{f\in \mathrm{Rels}|\wr f\in \mathrm{CnvRefRels}\right\}$$