Metamath Proof Explorer

Theorem 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 ⊢ φ → R Er X
erth.2 ⊢ φ → A ∈ X
Assertion erth ⊢ φ → A R B ↔ A R = B R

Proof

Step Hyp Ref Expression
1 erth.1 ⊢ φ → R Er X
2 erth.2 ⊢ φ → A ∈ X
3 1 ersymb ⊢ φ → A R B ↔ B R A
4 3 biimpa ⊢ φ ∧ A R B → B R A
5 1 ertr ⊢ φ → B R A ∧ A R x → B R x
6 5 impl ⊢ φ ∧ B R A ∧ A R x → B R x
7 4 6 syldanl ⊢ φ ∧ A R B ∧ A R x → B R x
8 1 ertr ⊢ φ → A R B ∧ B R x → A R x
9 8 impl ⊢ φ ∧ A R B ∧ B R x → A R x
10 7 9 impbida ⊢ φ ∧ A R B → A R x ↔ B R x
11 vex ⊢ x ∈ V
12 2 adantr ⊢ φ ∧ A R B → A ∈ X
13 elecg ⊢ x ∈ V ∧ A ∈ X → x ∈ A R ↔ A R x
14 11 12 13 sylancr ⊢ φ ∧ A R B → x ∈ A R ↔ A R x
15 errel ⊢ R Er X → Rel ⁡ R
16 1 15 syl ⊢ φ → Rel ⁡ R
17 brrelex2 ⊢ Rel ⁡ R ∧ A R B → B ∈ V
18 16 17 sylan ⊢ φ ∧ A R B → B ∈ V
19 elecg ⊢ x ∈ V ∧ B ∈ V → x ∈ B R ↔ B R x
20 11 18 19 sylancr ⊢ φ ∧ A R B → x ∈ B R ↔ B R x
21 10 14 20 3bitr4d ⊢ φ ∧ A R B → x ∈ A R ↔ x ∈ B R
22 21 eqrdv ⊢ φ ∧ A R B → A R = B R
23 1 adantr ⊢ φ ∧ A R = B R → R Er X
24 1 2 erref ⊢ φ → A R A
25 24 adantr ⊢ φ ∧ A R = B R → A R A
26 2 adantr ⊢ φ ∧ A R = B R → A ∈ X
27 elecg ⊢ A ∈ X ∧ A ∈ X → A ∈ A R ↔ A R A
28 26 26 27 syl2anc ⊢ φ ∧ A R = B R → A ∈ A R ↔ A R A
29 25 28 mpbird ⊢ φ ∧ A R = B R → A ∈ A R
30 simpr ⊢ φ ∧ A R = B R → A R = B R
31 29 30 eleqtrd ⊢ φ ∧ A R = B R → A ∈ B R
32 23 30 ereldm ⊢ φ ∧ A R = B R → A ∈ X ↔ B ∈ X
33 26 32 mpbid ⊢ φ ∧ A R = B R → B ∈ X
34 elecg ⊢ A ∈ X ∧ B ∈ X → A ∈ B R ↔ B R A
35 26 33 34 syl2anc ⊢ φ ∧ A R = B R → A ∈ B R ↔ B R A
36 31 35 mpbid ⊢ φ ∧ A R = B R → B R A
37 23 36 ersym ⊢ φ ∧ A R = B R → A R B
38 22 37 impbida ⊢ φ → A R B ↔ A R = B R