Description: A set is equal to its quotient set modulo the converse membership relation. (Note: the converse membership relation is not an equivalence relation.) (Contributed by NM, 13-Aug-1995) (Revised by Mario Carneiro, 9-Jul-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | qsid | |- ( A /. `' _E ) = A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | |- x e. _V |
|
| 2 | 1 | ecid | |- [ x ] `' _E = x |
| 3 | 2 | eqeq2i | |- ( y = [ x ] `' _E <-> y = x ) |
| 4 | equcom | |- ( y = x <-> x = y ) |
|
| 5 | 3 4 | bitri | |- ( y = [ x ] `' _E <-> x = y ) |
| 6 | 5 | rexbii | |- ( E. x e. A y = [ x ] `' _E <-> E. x e. A x = y ) |
| 7 | vex | |- y e. _V |
|
| 8 | 7 | elqs | |- ( y e. ( A /. `' _E ) <-> E. x e. A y = [ x ] `' _E ) |
| 9 | risset | |- ( y e. A <-> E. x e. A x = y ) |
|
| 10 | 6 8 9 | 3bitr4i | |- ( y e. ( A /. `' _E ) <-> y e. A ) |
| 11 | 10 | eqriv | |- ( A /. `' _E ) = A |