Description: Any set is equal to its preimage under the converse membership relation. (Contributed by Mario Carneiro, 9-Mar-2013) Put in closed form. (Revised by BJ, 16-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | epin | |- ( A e. V -> ( `' _E " { A } ) = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | |- x e. _V |
|
| 2 | 1 | eliniseg | |- ( A e. V -> ( x e. ( `' _E " { A } ) <-> x _E A ) ) |
| 3 | epelg | |- ( A e. V -> ( x _E A <-> x e. A ) ) |
|
| 4 | 2 3 | bitrd | |- ( A e. V -> ( x e. ( `' _E " { A } ) <-> x e. A ) ) |
| 5 | 4 | eqrdv | |- ( A e. V -> ( `' _E " { A } ) = A ) |