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 |