Theorem exdifsn

Description: There exists an element in a class excluding a singleton if and only if there exists an element in the original class not equal to the singleton element. (Contributed by BTernaryTau, 15-Sep-2023)

	Ref	Expression
Assertion	exdifsn	|- ( E. x x e. ( A \ { B } ) <-> E. x e. A x =/= B )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	|- ( x e. ( A \ { B } ) <-> ( x e. A /\ x =/= B ) )
2	1	exbii	|- ( E. x x e. ( A \ { B } ) <-> E. x ( x e. A /\ x =/= B ) )
3		df-rex	|- ( E. x e. A x =/= B <-> E. x ( x e. A /\ x =/= B ) )
4	2 3	bitr4i	|- ( E. x x e. ( A \ { B } ) <-> E. x e. A x =/= B )