Metamath Proof Explorer

Theorem 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 ⊢ φ → EqvRel R
eqvrelth.2 ⊢ φ → A ∈ dom ⁡ R
Assertion eqvrelth ⊢ φ → A R B ↔ A R = B R

Proof

Step Hyp Ref Expression
1 eqvrelth.1 ⊢ φ → EqvRel R
2 eqvrelth.2 ⊢ φ → A ∈ dom ⁡ R
3 1 eqvrelsymb ⊢ φ → A R B ↔ B R A
4 3 biimpa ⊢ φ ∧ A R B → B R A
5 1 eqvreltr ⊢ φ → 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 eqvreltr ⊢ φ → 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 ∈ dom ⁡ R
13 elecg ⊢ x ∈ V ∧ A ∈ dom ⁡ R → x ∈ A R ↔ A R x
14 11 12 13 sylancr ⊢ φ ∧ A R B → x ∈ A R ↔ A R x
15 eqvrelrel ⊢ EqvRel R → 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 → EqvRel R
24 1 2 eqvrelref ⊢ φ → A R A
25 24 adantr ⊢ φ ∧ A R = B R → A R A
26 2 adantr ⊢ φ ∧ A R = B R → A ∈ dom ⁡ R
27 elecALTV ⊢ A ∈ dom ⁡ R ∧ A ∈ dom ⁡ R → 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 30 dmec2d ⊢ φ ∧ A R = B R → A ∈ dom ⁡ R ↔ B ∈ dom ⁡ R
33 26 32 mpbid ⊢ φ ∧ A R = B R → B ∈ dom ⁡ R
34 elecALTV ⊢ B ∈ dom ⁡ R ∧ A ∈ dom ⁡ R → A ∈ B R ↔ B R A
35 33 26 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 eqvrelsym ⊢ φ ∧ A R = B R → A R B
38 22 37 impbida ⊢ φ → A R B ↔ A R = B R