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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ( V ∖ { 𝐵 } ) ↔ 𝐴 ≠ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	⊢ ( 𝐴 ∈ ( V ∖ { 𝐵 } ) ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ 𝐵 ) )
2		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
3	2	biantrurd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ 𝐵 ) ) )
4	1 3	bitr4id	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ( V ∖ { 𝐵 } ) ↔ 𝐴 ≠ 𝐵 ) )