# 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 ( 𝜑𝑅 Er 𝑋 )
erth.2 ( 𝜑𝐴𝑋 )
Assertion erth ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )

### Proof

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