erth

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)

	Ref	Expression
Hypotheses	erth.1	$⊢ φ \to R Er X$
	erth.2	$⊢ φ \to A \in X$
Assertion	erth	$⊢ φ \to (A R B \leftrightarrow [A] R = [B] R)$

Proof

Step	Hyp	Ref	Expression
1		erth.1	$⊢ φ \to R Er X$
2		erth.2	$⊢ φ \to A \in X$
3	1	ersymb	$⊢ φ \to (A R B \leftrightarrow B R A)$
4	3	biimpa	$⊢ (φ \land A R B) \to B R A$
5	1	ertr	$⊢ φ \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	ertr	$⊢ φ \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 X$
13		elecg	$⊢ (x \in V \land A \in X) \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		errel	$⊢ R Er X \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 R Er X$
24	1 2	erref	$⊢ φ \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 X$
27		elecg	$⊢ (A \in X \land A \in X) \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	23 30	ereldm	$⊢ (φ \land [A] R = [B] R) \to (A \in X \leftrightarrow B \in X)$
33	26 32	mpbid	$⊢ (φ \land [A] R = [B] R) \to B \in X$
34		elecg	$⊢ (A \in X \land B \in X) \to (A \in [B] R \leftrightarrow B R A)$
35	26 33 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	ersym	$⊢ (φ \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 erth

Proof