Theorem hashdifsn

Description: The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6-Jan-2018)

	Ref	Expression
Assertion	hashdifsn	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\right)\to \left|A\setminus \left\{B\right\}\right|=\left|A\right|-1$$

Proof

Step	Hyp	Ref	Expression
1		snssi	$$⊢B\in A\to \left\{B\right\}\subseteq A$$
2		hashssdif	$$⊢\left(A\in \mathrm{Fin}\wedge \left\{B\right\}\subseteq A\right)\to \left|A\setminus \left\{B\right\}\right|=\left|A\right|-\left|\left\{B\right\}\right|$$
3	1 2	sylan2	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\right)\to \left|A\setminus \left\{B\right\}\right|=\left|A\right|-\left|\left\{B\right\}\right|$$
4		hashsng	$$⊢B\in A\to \left|\left\{B\right\}\right|=1$$
5	4	adantl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\right)\to \left|\left\{B\right\}\right|=1$$
6	5	oveq2d	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\right)\to \left|A\right|-\left|\left\{B\right\}\right|=\left|A\right|-1$$
7	3 6	eqtrd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\right)\to \left|A\setminus \left\{B\right\}\right|=\left|A\right|-1$$