Theorem elfunsALTV

Description: Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021)

	Ref	Expression
Assertion	elfunsALTV	$$⊢F\in \mathrm{FunsALTV}\leftrightarrow \left(\wr F\in \mathrm{CnvRefRels}\wedge F\in \mathrm{Rels}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dffunsALTV	$$⊢\mathrm{FunsALTV}=\left\{x\in \mathrm{Rels}|\wr x\in \mathrm{CnvRefRels}\right\}$$
2		cosseq	$$⊢x=F\to \wr x=\wr F$$
3	2	eleq1d	$$⊢x=F\to \left(\wr x\in \mathrm{CnvRefRels}\leftrightarrow \wr F\in \mathrm{CnvRefRels}\right)$$
4	1 3	rabeqel	$$⊢F\in \mathrm{FunsALTV}\leftrightarrow \left(\wr F\in \mathrm{CnvRefRels}\wedge F\in \mathrm{Rels}\right)$$