Metamath Proof Explorer

Theorem eleqvrels3

Description: Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021)

		Ref	Expression
	Assertion	eleqvrels3	$⊢ R \in EqvRels \leftrightarrow ((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x) \land \forall x \forall y \forall z ((x R y \land y R z) \to x R z)) \land R \in Rels)$

Proof

Step	Hyp	Ref	Expression
1		dfeqvrels3	$⊢ EqvRels = \{r \in Rels \| (\forall x \in dom r x r x \land \forall x \forall y (x r y \to y r x) \land \forall x \forall y \forall z ((x r y \land y r z) \to x r z))\}$
2		dmeq	$⊢ r = R \to dom r = dom R$
3		breq	$⊢ r = R \to (x r x \leftrightarrow x R x)$
4	2 3	raleqbidv	$⊢ r = R \to (\forall x \in dom r x r x \leftrightarrow \forall x \in dom R x R x)$
5		breq	$⊢ r = R \to (x r y \leftrightarrow x R y)$
6		breq	$⊢ r = R \to (y r x \leftrightarrow y R x)$
7	5 6	imbi12d	$⊢ r = R \to ((x r y \to y r x) \leftrightarrow (x R y \to y R x))$
8	7	2albidv	$⊢ r = R \to (\forall x \forall y (x r y \to y r x) \leftrightarrow \forall x \forall y (x R y \to y R x))$
9		breq	$⊢ r = R \to (y r z \leftrightarrow y R z)$
10	5 9	anbi12d	$⊢ r = R \to ((x r y \land y r z) \leftrightarrow (x R y \land y R z))$
11		breq	$⊢ r = R \to (x r z \leftrightarrow x R z)$
12	10 11	imbi12d	$⊢ r = R \to (((x r y \land y r z) \to x r z) \leftrightarrow ((x R y \land y R z) \to x R z))$
13	12	2albidv	$⊢ r = R \to (\forall y \forall z ((x r y \land y r z) \to x r z) \leftrightarrow \forall y \forall z ((x R y \land y R z) \to x R z))$
14	13	albidv	$⊢ r = R \to (\forall x \forall y \forall z ((x r y \land y r z) \to x r z) \leftrightarrow \forall x \forall y \forall z ((x R y \land y R z) \to x R z))$
15	4 8 14	3anbi123d	$⊢ r = R \to ((\forall x \in dom r x r x \land \forall x \forall y (x r y \to y r x) \land \forall x \forall y \forall z ((x r y \land y r z) \to x r z)) \leftrightarrow (\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x) \land \forall x \forall y \forall z ((x R y \land y R z) \to x R z)))$
16	1 15	rabeqel	$⊢ R \in EqvRels \leftrightarrow ((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x) \land \forall x \forall y \forall z ((x R y \land y R z) \to x R z)) \land R \in Rels)$