# 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 ${⊢}{\phi }\to {R}\mathrm{Er}{X}$
erth.2 ${⊢}{\phi }\to {A}\in {X}$
Assertion erth ${⊢}{\phi }\to \left({A}{R}{B}↔\left[{A}\right]{R}=\left[{B}\right]{R}\right)$

### Proof

Step Hyp Ref Expression
1 erth.1 ${⊢}{\phi }\to {R}\mathrm{Er}{X}$
2 erth.2 ${⊢}{\phi }\to {A}\in {X}$
3 1 ersymb ${⊢}{\phi }\to \left({A}{R}{B}↔{B}{R}{A}\right)$
4 3 biimpa ${⊢}\left({\phi }\wedge {A}{R}{B}\right)\to {B}{R}{A}$
5 1 ertr ${⊢}{\phi }\to \left(\left({B}{R}{A}\wedge {A}{R}{x}\right)\to {B}{R}{x}\right)$
6 5 impl ${⊢}\left(\left({\phi }\wedge {B}{R}{A}\right)\wedge {A}{R}{x}\right)\to {B}{R}{x}$
7 4 6 syldanl ${⊢}\left(\left({\phi }\wedge {A}{R}{B}\right)\wedge {A}{R}{x}\right)\to {B}{R}{x}$
8 1 ertr ${⊢}{\phi }\to \left(\left({A}{R}{B}\wedge {B}{R}{x}\right)\to {A}{R}{x}\right)$
9 8 impl ${⊢}\left(\left({\phi }\wedge {A}{R}{B}\right)\wedge {B}{R}{x}\right)\to {A}{R}{x}$
10 7 9 impbida ${⊢}\left({\phi }\wedge {A}{R}{B}\right)\to \left({A}{R}{x}↔{B}{R}{x}\right)$
11 vex ${⊢}{x}\in \mathrm{V}$
12 2 adantr ${⊢}\left({\phi }\wedge {A}{R}{B}\right)\to {A}\in {X}$
13 elecg ${⊢}\left({x}\in \mathrm{V}\wedge {A}\in {X}\right)\to \left({x}\in \left[{A}\right]{R}↔{A}{R}{x}\right)$
14 11 12 13 sylancr ${⊢}\left({\phi }\wedge {A}{R}{B}\right)\to \left({x}\in \left[{A}\right]{R}↔{A}{R}{x}\right)$
15 errel ${⊢}{R}\mathrm{Er}{X}\to \mathrm{Rel}{R}$
16 1 15 syl ${⊢}{\phi }\to \mathrm{Rel}{R}$
17 brrelex2 ${⊢}\left(\mathrm{Rel}{R}\wedge {A}{R}{B}\right)\to {B}\in \mathrm{V}$
18 16 17 sylan ${⊢}\left({\phi }\wedge {A}{R}{B}\right)\to {B}\in \mathrm{V}$
19 elecg ${⊢}\left({x}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to \left({x}\in \left[{B}\right]{R}↔{B}{R}{x}\right)$
20 11 18 19 sylancr ${⊢}\left({\phi }\wedge {A}{R}{B}\right)\to \left({x}\in \left[{B}\right]{R}↔{B}{R}{x}\right)$
21 10 14 20 3bitr4d ${⊢}\left({\phi }\wedge {A}{R}{B}\right)\to \left({x}\in \left[{A}\right]{R}↔{x}\in \left[{B}\right]{R}\right)$
22 21 eqrdv ${⊢}\left({\phi }\wedge {A}{R}{B}\right)\to \left[{A}\right]{R}=\left[{B}\right]{R}$
23 1 adantr ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to {R}\mathrm{Er}{X}$
24 1 2 erref ${⊢}{\phi }\to {A}{R}{A}$
25 24 adantr ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to {A}{R}{A}$
26 2 adantr ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to {A}\in {X}$
27 elecg ${⊢}\left({A}\in {X}\wedge {A}\in {X}\right)\to \left({A}\in \left[{A}\right]{R}↔{A}{R}{A}\right)$
28 26 26 27 syl2anc ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to \left({A}\in \left[{A}\right]{R}↔{A}{R}{A}\right)$
29 25 28 mpbird ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to {A}\in \left[{A}\right]{R}$
30 simpr ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to \left[{A}\right]{R}=\left[{B}\right]{R}$
31 29 30 eleqtrd ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to {A}\in \left[{B}\right]{R}$
32 23 30 ereldm ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to \left({A}\in {X}↔{B}\in {X}\right)$
33 26 32 mpbid ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to {B}\in {X}$
34 elecg ${⊢}\left({A}\in {X}\wedge {B}\in {X}\right)\to \left({A}\in \left[{B}\right]{R}↔{B}{R}{A}\right)$
35 26 33 34 syl2anc ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to \left({A}\in \left[{B}\right]{R}↔{B}{R}{A}\right)$
36 31 35 mpbid ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to {B}{R}{A}$
37 23 36 ersym ${⊢}\left({\phi }\wedge \left[{A}\right]{R}=\left[{B}\right]{R}\right)\to {A}{R}{B}$
38 22 37 impbida ${⊢}{\phi }\to \left({A}{R}{B}↔\left[{A}\right]{R}=\left[{B}\right]{R}\right)$