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

Metamath Proof Explorer

Theorem sneqrg

Description: Closed form of sneqr . (Contributed by Scott Fenton, 1-Apr-2011) (Proof shortened by JJ, 23-Jul-2021)

Ref Expression
Assertion sneqrg ⊢ A ∈ V → A = B → A = B

Proof

Step Hyp Ref Expression
1 snidg ⊢ A ∈ V → A ∈ A
2 eleq2 ⊢ A = B → A ∈ A ↔ A ∈ B
3 1 2 syl5ibcom ⊢ A ∈ V → A = B → A ∈ B
4 elsng ⊢ A ∈ V → A ∈ B ↔ A = B
5 3 4 sylibd ⊢ A ∈ V → A = B → A = B