Description: The closest one can get to isset without using ax-ext . See also vexw . Note that the only disjoint variable condition is between y and A . From there, one can prove isset using eleq2i (which requires ax-ext and df-cleq ). (Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bj-issetw.1 | |- ph |
|
Assertion | bj-issetw | |- ( A e. { x | ph } <-> E. y y = A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-issetw.1 | |- ph |
|
2 | bj-issetwt | |- ( A. x ph -> ( A e. { x | ph } <-> E. y y = A ) ) |
|
3 | 2 1 | mpg | |- ( A e. { x | ph } <-> E. y y = A ) |