This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfunsALTV

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

		Ref	Expression
	Assertion	elfunsALTV	$⊢ F \in FunsALTV \leftrightarrow (≀ F \in CnvRefRels \land F \in Rels)$

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