Description: A set is equal to its coset under 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 | ||
|---|---|---|---|
| Hypothesis | ecid.1 | |- A e. _V |
|
| Assertion | ecid | |- [ A ] `' _E = A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ecid.1 | |- A e. _V |
|
| 2 | vex | |- y e. _V |
|
| 3 | 2 1 | elec | |- ( y e. [ A ] `' _E <-> A `' _E y ) |
| 4 | 1 2 | brcnv | |- ( A `' _E y <-> y _E A ) |
| 5 | 1 | epeli | |- ( y _E A <-> y e. A ) |
| 6 | 3 4 5 | 3bitri | |- ( y e. [ A ] `' _E <-> y e. A ) |
| 7 | 6 | eqriv | |- [ A ] `' _E = A |