Description: One direction of cleljust , requiring only ax-1 -- ax-5 and ax8v1 . (Contributed by BJ, 31-Dec-2020) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-cleljusti | |- ( E. z ( z = x /\ z e. y ) -> x e. y ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax8v1 | |- ( z = x -> ( z e. y -> x e. y ) ) |
|
2 | 1 | imp | |- ( ( z = x /\ z e. y ) -> x e. y ) |
3 | 2 | exlimiv | |- ( E. z ( z = x /\ z e. y ) -> x e. y ) |