Metamath Proof Explorer

Theorem dffun2OLD

Description: Obsolete version of dffun2 as of 29-Dec-2024. (Contributed by NM, 29-Dec-1996) Avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	dffun2OLD	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \forall y \forall z ((x A y \land x A z) \to y = z))$

Proof

Step	Hyp	Ref	Expression
1		df-fun	$⊢ Fun A \leftrightarrow (Rel A \land A \circ A^{-1} \subseteq I)$
2		cotrg	$⊢ A \circ A^{-1} \subseteq I \leftrightarrow \forall y \forall x \forall z ((y A^{-1} x \land x A z) \to y I z)$
3		alcom	$⊢ \forall y \forall x \forall z ((y A^{-1} x \land x A z) \to y I z) \leftrightarrow \forall x \forall y \forall z ((y A^{-1} x \land x A z) \to y I z)$
4		vex	$⊢ y \in V$
5		vex	$⊢ x \in V$
6	4 5	brcnv	$⊢ y A^{-1} x \leftrightarrow x A y$
7	6	anbi1i	$⊢ (y A^{-1} x \land x A z) \leftrightarrow (x A y \land x A z)$
8		vex	$⊢ z \in V$
9	8	ideq	$⊢ y I z \leftrightarrow y = z$
10	7 9	imbi12i	$⊢ ((y A^{-1} x \land x A z) \to y I z) \leftrightarrow ((x A y \land x A z) \to y = z)$
11	10	3albii	$⊢ \forall x \forall y \forall z ((y A^{-1} x \land x A z) \to y I z) \leftrightarrow \forall x \forall y \forall z ((x A y \land x A z) \to y = z)$
12	3 11	bitri	$⊢ \forall y \forall x \forall z ((y A^{-1} x \land x A z) \to y I z) \leftrightarrow \forall x \forall y \forall z ((x A y \land x A z) \to y = z)$
13	2 12	bitri	$⊢ A \circ A^{-1} \subseteq I \leftrightarrow \forall x \forall y \forall z ((x A y \land x A z) \to y = z)$
14	13	anbi2i	$⊢ (Rel A \land A \circ A^{-1} \subseteq I) \leftrightarrow (Rel A \land \forall x \forall y \forall z ((x A y \land x A z) \to y = z))$
15	1 14	bitri	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \forall y \forall z ((x A y \land x A z) \to y = z))$