elfunsALTV4

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

		Ref	Expression
	Assertion	elfunsALTV4	$⊢ F \in FunsALTV \leftrightarrow (\forall u \exists^{*} x u F x \land F \in Rels)$

Step	Hyp	Ref	Expression
1		elfunsALTV	$⊢ F \in FunsALTV \leftrightarrow (≀ F \in CnvRefRels \land F \in Rels)$
2		cosselcnvrefrels4	$⊢ ≀ F \in CnvRefRels \leftrightarrow (\forall u \exists^{*} x u F x \land ≀ F \in Rels)$
3		cosselrels	$⊢ F \in Rels \to ≀ F \in Rels$
4	3	biantrud	$⊢ F \in Rels \to (\forall u \exists^{} x u F x \leftrightarrow (\forall u \exists^{} x u F x \land ≀ F \in Rels))$
5	2 4	bitr4id	$⊢ F \in Rels \to (≀ F \in CnvRefRels \leftrightarrow \forall u \exists^{*} x u F x)$
6	5	pm5.32ri	$⊢ (≀ F \in CnvRefRels \land F \in Rels) \leftrightarrow (\forall u \exists^{*} x u F x \land F \in Rels)$
7	1 6	bitri	$⊢ F \in FunsALTV \leftrightarrow (\forall u \exists^{*} x u F x \land F \in Rels)$

Metamath Proof Explorer