Theorem diffib

Description: Case where diffi is a biconditional. (Contributed by Thierry Arnoux, 27-Jun-2024)

	Ref	Expression
Assertion	diffib	$$⊢B\in \mathrm{Fin}\to \left(A\in \mathrm{Fin}\leftrightarrow A\setminus B\in \mathrm{Fin}\right)$$

Proof

Step	Hyp	Ref	Expression
1		diffi	$$⊢A\in \mathrm{Fin}\to A\setminus B\in \mathrm{Fin}$$
2	1	adantl	$$⊢\left(B\in \mathrm{Fin}\wedge A\in \mathrm{Fin}\right)\to A\setminus B\in \mathrm{Fin}$$
3		difinf	$$⊢\left(\neg A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \neg A\setminus B\in \mathrm{Fin}$$
4	3	ancoms	$$⊢\left(B\in \mathrm{Fin}\wedge \neg A\in \mathrm{Fin}\right)\to \neg A\setminus B\in \mathrm{Fin}$$
5	4	ex	$$⊢B\in \mathrm{Fin}\to \left(\neg A\in \mathrm{Fin}\to \neg A\setminus B\in \mathrm{Fin}\right)$$
6	5	con4d	$$⊢B\in \mathrm{Fin}\to \left(A\setminus B\in \mathrm{Fin}\to A\in \mathrm{Fin}\right)$$
7	6	imp	$$⊢\left(B\in \mathrm{Fin}\wedge A\setminus B\in \mathrm{Fin}\right)\to A\in \mathrm{Fin}$$
8	2 7	impbida	$$⊢B\in \mathrm{Fin}\to \left(A\in \mathrm{Fin}\leftrightarrow A\setminus B\in \mathrm{Fin}\right)$$