Theorem difsnpss

Description: ( B \ { A } ) is a proper subclass of B if and only if A is a member of B . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Assertion	difsnpss	$$⊢A\in B\leftrightarrow B\setminus \left\{A\right\}\subset B$$

Proof

Step	Hyp	Ref	Expression
1		notnotb	$$⊢A\in B\leftrightarrow \neg \neg A\in B$$
2		difss	$$⊢B\setminus \left\{A\right\}\subseteq B$$
3	2	biantrur	$$⊢B\setminus \left\{A\right\}\ne B\leftrightarrow \left(B\setminus \left\{A\right\}\subseteq B\wedge B\setminus \left\{A\right\}\ne B\right)$$
4		difsnb	$$⊢\neg A\in B\leftrightarrow B\setminus \left\{A\right\}=B$$
5	4	necon3bbii	$$⊢\neg \neg A\in B\leftrightarrow B\setminus \left\{A\right\}\ne B$$
6		df-pss	$$⊢B\setminus \left\{A\right\}\subset B\leftrightarrow \left(B\setminus \left\{A\right\}\subseteq B\wedge B\setminus \left\{A\right\}\ne B\right)$$
7	3 5 6	3bitr4i	$$⊢\neg \neg A\in B\leftrightarrow B\setminus \left\{A\right\}\subset B$$
8	1 7	bitri	$$⊢A\in B\leftrightarrow B\setminus \left\{A\right\}\subset B$$