elfunsALTV3

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

		Ref	Expression
	Assertion	elfunsALTV3	$⊢ F \in FunsALTV \leftrightarrow (\forall u \forall x \forall y ((u F x \land u F y) \to x = y) \land F \in Rels)$

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

Metamath Proof Explorer