# Metamath Proof Explorer

## Theorem erdisj

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)

Ref Expression
Assertion erdisj ${⊢}{R}\mathrm{Er}{X}\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({R}\mathrm{Er}{X}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {R}\mathrm{Er}{X}$
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({R}\mathrm{Er}{X}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {x}\in \left[{A}\right]{R}$
5 vex ${⊢}{x}\in \mathrm{V}$
6 ecexr ${⊢}{x}\in \left[{A}\right]{R}\to {A}\in \mathrm{V}$
7 4 6 syl ${⊢}\left({R}\mathrm{Er}{X}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {A}\in \mathrm{V}$
8 elecg ${⊢}\left({x}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to \left({x}\in \left[{A}\right]{R}↔{A}{R}{x}\right)$
9 5 7 8 sylancr ${⊢}\left({R}\mathrm{Er}{X}\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({R}\mathrm{Er}{X}\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({R}\mathrm{Er}{X}\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({R}\mathrm{Er}{X}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {B}\in \mathrm{V}$
15 elecg ${⊢}\left({x}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to \left({x}\in \left[{B}\right]{R}↔{B}{R}{x}\right)$
16 5 14 15 sylancr ${⊢}\left({R}\mathrm{Er}{X}\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({R}\mathrm{Er}{X}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {B}{R}{x}$
18 2 10 17 ertr4d ${⊢}\left({R}\mathrm{Er}{X}\wedge {x}\in \left(\left[{A}\right]{R}\cap \left[{B}\right]{R}\right)\right)\to {A}{R}{B}$
19 2 18 erthi ${⊢}\left({R}\mathrm{Er}{X}\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 ${⊢}{R}\mathrm{Er}{X}\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 ${⊢}{R}\mathrm{Er}{X}\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 ${⊢}{R}\mathrm{Er}{X}\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 ${⊢}{R}\mathrm{Er}{X}\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 ${⊢}{R}\mathrm{Er}{X}\to \left(\left[{A}\right]{R}=\left[{B}\right]{R}\vee \left[{A}\right]{R}\cap \left[{B}\right]{R}=\varnothing \right)$