Metamath Proof Explorer
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 |
⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦 ) → 𝑥 ∈ 𝑦 ) |