# Metamath Proof Explorer

## Theorem eqvreldisj

Description: Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of Suppes p. 83. (Contributed by NM, 15-Jun-2004) (Revised by Mario Carneiro, 9-Jul-2014) (Revised by Peter Mazsa, 2-Jun-2019)

Ref Expression
Assertion eqvreldisj ${⊢}EqvRel{R}\to \left(\left[{A}\right]{R}=\left[{B}\right]{R}\vee \left[{A}\right]{R}\cap \left[{B}\right]{R}=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 neq0 ${⊢}¬\left[{A}\right]{R}\cap \left[{B}\right]{R}=\varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)$
2 simpl ${⊢}\left(EqvRel{R}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to EqvRel{R}$
3 elinel1 ${⊢}{x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\to {x}\in \left[{A}\right]{R}$
4 3 adantl ${⊢}\left(EqvRel{R}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {x}\in \left[{A}\right]{R}$
5 ecexr ${⊢}{x}\in \left[{A}\right]{R}\to {A}\in \mathrm{V}$
6 4 5 syl ${⊢}\left(EqvRel{R}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {A}\in \mathrm{V}$
7 vex ${⊢}{x}\in \mathrm{V}$
8 elecALTV ${⊢}\left({A}\in \mathrm{V}\wedge {x}\in \mathrm{V}\right)\to \left({x}\in \left[{A}\right]{R}↔{A}{R}{x}\right)$
9 6 7 8 sylancl ${⊢}\left(EqvRel{R}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to \left({x}\in \left[{A}\right]{R}↔{A}{R}{x}\right)$
10 4 9 mpbid ${⊢}\left(EqvRel{R}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {A}{R}{x}$
11 elinel2 ${⊢}{x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\to {x}\in \left[{B}\right]{R}$
12 11 adantl ${⊢}\left(EqvRel{R}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {x}\in \left[{B}\right]{R}$
13 ecexr ${⊢}{x}\in \left[{B}\right]{R}\to {B}\in \mathrm{V}$
14 12 13 syl ${⊢}\left(EqvRel{R}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {B}\in \mathrm{V}$
15 elecALTV ${⊢}\left({B}\in \mathrm{V}\wedge {x}\in \mathrm{V}\right)\to \left({x}\in \left[{B}\right]{R}↔{B}{R}{x}\right)$
16 14 7 15 sylancl ${⊢}\left(EqvRel{R}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to \left({x}\in \left[{B}\right]{R}↔{B}{R}{x}\right)$
17 12 16 mpbid ${⊢}\left(EqvRel{R}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {B}{R}{x}$
18 2 10 17 eqvreltr4d ${⊢}\left(EqvRel{R}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {A}{R}{B}$
19 2 18 eqvrelthi ${⊢}\left(EqvRel{R}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to \left[{A}\right]{R}=\left[{B}\right]{R}$
20 19 ex ${⊢}EqvRel{R}\to \left({x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\to \left[{A}\right]{R}=\left[{B}\right]{R}\right)$
21 20 exlimdv ${⊢}EqvRel{R}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\to \left[{A}\right]{R}=\left[{B}\right]{R}\right)$
22 1 21 syl5bi ${⊢}EqvRel{R}\to \left(¬\left[{A}\right]{R}\cap \left[{B}\right]{R}=\varnothing \to \left[{A}\right]{R}=\left[{B}\right]{R}\right)$
23 22 orrd ${⊢}EqvRel{R}\to \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}=\varnothing \vee \left[{A}\right]{R}=\left[{B}\right]{R}\right)$
24 23 orcomd ${⊢}EqvRel{R}\to \left(\left[{A}\right]{R}=\left[{B}\right]{R}\vee \left[{A}\right]{R}\cap \left[{B}\right]{R}=\varnothing \right)$