Metamath Proof Explorer


Theorem ecid

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

Proof

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