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 e. V -> ( A e. ( _V \ { B } ) <-> A =/= B ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	|- ( A e. ( _V \ { B } ) <-> ( A e. _V /\ A =/= B ) )
2		elex	|- ( A e. V -> A e. _V )
3	2	biantrurd	|- ( A e. V -> ( A =/= B <-> ( A e. _V /\ A =/= B ) ) )
4	1 3	bitr4id	|- ( A e. V -> ( A e. ( _V \ { B } ) <-> A =/= B ) )