Theorem ssdifsn

Description: Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021) (Proof shortened by JJ, 31-May-2022)

	Ref	Expression
Assertion	ssdifsn	$$⊢A\subseteq B\setminus \left\{C\right\}\leftrightarrow \left(A\subseteq B\wedge \neg C\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		difss2	$$⊢A\subseteq B\setminus \left\{C\right\}\to A\subseteq B$$
2		reldisj	$$⊢A\subseteq B\to \left(A\cap \left\{C\right\}=\varnothing \leftrightarrow A\subseteq B\setminus \left\{C\right\}\right)$$
3	2	bicomd	$$⊢A\subseteq B\to \left(A\subseteq B\setminus \left\{C\right\}\leftrightarrow A\cap \left\{C\right\}=\varnothing \right)$$
4	1 3	biadanii	$$⊢A\subseteq B\setminus \left\{C\right\}\leftrightarrow \left(A\subseteq B\wedge A\cap \left\{C\right\}=\varnothing \right)$$
5		disjsn	$$⊢A\cap \left\{C\right\}=\varnothing \leftrightarrow \neg C\in A$$
6	5	anbi2i	$$⊢\left(A\subseteq B\wedge A\cap \left\{C\right\}=\varnothing \right)\leftrightarrow \left(A\subseteq B\wedge \neg C\in A\right)$$
7	4 6	bitri	$$⊢A\subseteq B\setminus \left\{C\right\}\leftrightarrow \left(A\subseteq B\wedge \neg C\in A\right)$$