Metamath Proof Explorer

Theorem elfunsALTVfunALTV

Description: The element of the class of functions and the function predicate are the same when F is a set. (Contributed by Peter Mazsa, 26-Jul-2021)

		Ref	Expression
	Assertion	elfunsALTVfunALTV	$⊢ F \in V \to (F \in FunsALTV \leftrightarrow FunALTV F)$

Proof

Step	Hyp	Ref	Expression
1		cossex	$⊢ F \in V \to ≀ F \in V$
2		elcnvrefrelsrel	$⊢ ≀ F \in V \to (≀ F \in CnvRefRels \leftrightarrow CnvRefRel ≀ F)$
3	1 2	syl	$⊢ F \in V \to (≀ F \in CnvRefRels \leftrightarrow CnvRefRel ≀ F)$
4		elrelsrel	$⊢ F \in V \to (F \in Rels \leftrightarrow Rel F)$
5	3 4	anbi12d	$⊢ F \in V \to ((≀ F \in CnvRefRels \land F \in Rels) \leftrightarrow (CnvRefRel ≀ F \land Rel F))$
6		elfunsALTV	$⊢ F \in FunsALTV \leftrightarrow (≀ F \in CnvRefRels \land F \in Rels)$
7		df-funALTV	$⊢ FunALTV F \leftrightarrow (CnvRefRel ≀ F \land Rel F)$
8	5 6 7	3bitr4g	$⊢ F \in V \to (F \in FunsALTV \leftrightarrow FunALTV F)$