Description: The elements of the quotient set of an equivalence relation are disjoint (cf. qsdisj2 ). (Contributed by Mario Carneiro, 10-Dec-2016) (Revised by Peter Mazsa, 20-Jun-2019) (Revised by Peter Mazsa, 19-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eqvreldisj3 | |- ( EqvRel R -> Disj ( `' _E |` ( A /. R ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqvreldisj2 | |- ( EqvRel R -> ElDisj ( A /. R ) ) |
|
| 2 | df-eldisj | |- ( ElDisj ( A /. R ) <-> Disj ( `' _E |` ( A /. R ) ) ) |
|
| 3 | 1 2 | sylib | |- ( EqvRel R -> Disj ( `' _E |` ( A /. R ) ) ) |