Description: An element of a class exists. Use elissetv instead when sufficient (for instance in usages where x is a dummy variable). (Contributed by NM, 1-May-1995) Reduce dependencies on axioms. (Revised by BJ, 29-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | elisset | |- ( A e. V -> E. x x = A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elissetv | |- ( A e. V -> E. y y = A ) |
|
2 | vextru | |- y e. { z | T. } |
|
3 | 2 | issetlem | |- ( A e. { z | T. } <-> E. y y = A ) |
4 | vextru | |- x e. { z | T. } |
|
5 | 4 | issetlem | |- ( A e. { z | T. } <-> E. x x = A ) |
6 | 3 5 | bitr3i | |- ( E. y y = A <-> E. x x = A ) |
7 | 1 6 | sylib | |- ( A e. V -> E. x x = A ) |