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

Metamath Proof Explorer

Theorem eldifvsn

Description: A set is an element of the universal class excluding a singleton iff it is not the singleton element. (Contributed by AV, 7-Apr-2019)

Ref Expression
Assertion eldifvsn ⊢ A ∈ V → A ∈ V ∖ B ↔ A ≠ B

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ A ∈ V ∖ B ↔ A ∈ V ∧ A ≠ B
2 elex ⊢ A ∈ V → A ∈ V
3 2 biantrurd ⊢ A ∈ V → A ≠ B ↔ A ∈ V ∧ A ≠ B
4 1 3 bitr4id ⊢ A ∈ V → A ∈ V ∖ B ↔ A ≠ B