Metamath Proof Explorer

Theorem dffunsALTV3

Description: Alternate definition of the class of functions. For the X axis and the Y axis you can convert the right side to { f e. Rels | A. x1 A. y1 A. y2 ( ( x1 f y1 /\ x1 f y2 ) -> y1 = y2 ) } . (Contributed by Peter Mazsa, 30-Aug-2021)

		Ref	Expression
	Assertion	dffunsALTV3	$⊢ FunsALTV = \{f \in Rels \| \forall u \forall x \forall y ((u f x \land u f y) \to x = y)\}$

Proof

Step	Hyp	Ref	Expression
1		dffunsALTV	$⊢ FunsALTV = \{f \in Rels \| ≀ f \in CnvRefRels\}$
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	1 5	rabimbieq	$⊢ FunsALTV = \{f \in Rels \| \forall u \forall x \forall y ((u f x \land u f y) \to x = y)\}$