Description: An element of a class exists. (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 | exsimpl | |- ( E. y ( y = A /\ y e. V ) -> E. y y = A ) |
|
2 | dfclel | |- ( A e. V <-> E. y ( y = A /\ y e. V ) ) |
|
3 | eqeq1 | |- ( x = y -> ( x = A <-> y = A ) ) |
|
4 | 3 | cbvexvw | |- ( E. x x = A <-> E. y y = A ) |
5 | 1 2 4 | 3imtr4i | |- ( A e. V -> E. x x = A ) |