Description: Alternate proof of elisset . This is essentially the same proof as seen by inlining bj-denotes and bj-denoteslem . Use elissetv instead when sufficient (in particular when V is substituted for _V ). (Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-elissetALT | |- ( A e. V -> E. x x = A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elissetv | |- ( A e. V -> E. y y = A ) |
|
2 | bj-denotes | |- ( E. y y = A <-> E. x x = A ) |
|
3 | 1 2 | sylib | |- ( A e. V -> E. x x = A ) |