eqvrelth

Description: Basic property of equivalence relations. Theorem 73 of Suppes p. 82. (Contributed by NM, 23-Jul-1995) (Revised by Mario Carneiro, 6-Jul-2015) (Revised by Peter Mazsa, 2-Jun-2019)

	Ref	Expression
Hypotheses	eqvrelth.1	$⊢ φ \to EqvRel R$
	eqvrelth.2	$⊢ φ \to A \in dom R$
Assertion	eqvrelth	$⊢ φ \to (A R B \leftrightarrow [A] R = [B] R)$

Proof

Step	Hyp	Ref	Expression
1		eqvrelth.1	$⊢ φ \to EqvRel R$
2		eqvrelth.2	$⊢ φ \to A \in dom R$
3	1	eqvrelsymb	$⊢ φ \to (A R B \leftrightarrow B R A)$
4	3	biimpa	$⊢ (φ \land A R B) \to B R A$
5	1	eqvreltr	$⊢ φ \to ((B R A \land A R x) \to B R x)$
6	5	impl	$⊢ ((φ \land B R A) \land A R x) \to B R x$
7	4 6	syldanl	$⊢ ((φ \land A R B) \land A R x) \to B R x$
8	1	eqvreltr	$⊢ φ \to ((A R B \land B R x) \to A R x)$
9	8	impl	$⊢ ((φ \land A R B) \land B R x) \to A R x$
10	7 9	impbida	$⊢ (φ \land A R B) \to (A R x \leftrightarrow B R x)$
11		vex	$⊢ x \in V$
12	2	adantr	$⊢ (φ \land A R B) \to A \in dom R$
13		elecg	$⊢ (x \in V \land A \in dom R) \to (x \in [A] R \leftrightarrow A R x)$
14	11 12 13	sylancr	$⊢ (φ \land A R B) \to (x \in [A] R \leftrightarrow A R x)$
15		eqvrelrel	$⊢ EqvRel R \to Rel R$
16	1 15	syl	$⊢ φ \to Rel R$
17		brrelex2	$⊢ (Rel R \land A R B) \to B \in V$
18	16 17	sylan	$⊢ (φ \land A R B) \to B \in V$
19		elecg	$⊢ (x \in V \land B \in V) \to (x \in [B] R \leftrightarrow B R x)$
20	11 18 19	sylancr	$⊢ (φ \land A R B) \to (x \in [B] R \leftrightarrow B R x)$
21	10 14 20	3bitr4d	$⊢ (φ \land A R B) \to (x \in [A] R \leftrightarrow x \in [B] R)$
22	21	eqrdv	$⊢ (φ \land A R B) \to [A] R = [B] R$
23	1	adantr	$⊢ (φ \land [A] R = [B] R) \to EqvRel R$
24	1 2	eqvrelref	$⊢ φ \to A R A$
25	24	adantr	$⊢ (φ \land [A] R = [B] R) \to A R A$
26	2	adantr	$⊢ (φ \land [A] R = [B] R) \to A \in dom R$
27		elecALTV	$⊢ (A \in dom R \land A \in dom R) \to (A \in [A] R \leftrightarrow A R A)$
28	26 26 27	syl2anc	$⊢ (φ \land [A] R = [B] R) \to (A \in [A] R \leftrightarrow A R A)$
29	25 28	mpbird	$⊢ (φ \land [A] R = [B] R) \to A \in [A] R$
30		simpr	$⊢ (φ \land [A] R = [B] R) \to [A] R = [B] R$
31	29 30	eleqtrd	$⊢ (φ \land [A] R = [B] R) \to A \in [B] R$
32	30	dmec2d	$⊢ (φ \land [A] R = [B] R) \to (A \in dom R \leftrightarrow B \in dom R)$
33	26 32	mpbid	$⊢ (φ \land [A] R = [B] R) \to B \in dom R$
34		elecALTV	$⊢ (B \in dom R \land A \in dom R) \to (A \in [B] R \leftrightarrow B R A)$
35	33 26 34	syl2anc	$⊢ (φ \land [A] R = [B] R) \to (A \in [B] R \leftrightarrow B R A)$
36	31 35	mpbid	$⊢ (φ \land [A] R = [B] R) \to B R A$
37	23 36	eqvrelsym	$⊢ (φ \land [A] R = [B] R) \to A R B$
38	22 37	impbida	$⊢ φ \to (A R B \leftrightarrow [A] R = [B] R)$

Metamath Proof Explorer

Theorem eqvrelth

Proof