This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-ax6elem2

Description: Lemma for bj-ax6e . (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ax6elem2 ⊢ ∀ x y = z → ∃ x x = y

Proof

Step Hyp Ref Expression
1 ax6ev ⊢ ∃ x x = z
2 equeucl ⊢ x = z → y = z → x = y
3 1 2 eximii ⊢ ∃ x y = z → x = y
4 3 19.35i ⊢ ∀ x y = z → ∃ x x = y