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 ( ∃ 𝑧 ( 𝑧 = 𝑥𝑧𝑦 ) → 𝑥𝑦 )

Proof

Step Hyp Ref Expression
1 ax8v1 ( 𝑧 = 𝑥 → ( 𝑧𝑦𝑥𝑦 ) )
2 1 imp ( ( 𝑧 = 𝑥𝑧𝑦 ) → 𝑥𝑦 )
3 2 exlimiv ( ∃ 𝑧 ( 𝑧 = 𝑥𝑧𝑦 ) → 𝑥𝑦 )