Metamath Proof Explorer


Theorem bj-cleljusti

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 )

Proof

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 )