Theorem diffib

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

	Ref	Expression
Assertion	diffib	|- ( B e. Fin -> ( A e. Fin <-> ( A \ B ) e. Fin ) )

Proof

Step	Hyp	Ref	Expression
1		diffi	|- ( A e. Fin -> ( A \ B ) e. Fin )
2	1	adantl	|- ( ( B e. Fin /\ A e. Fin ) -> ( A \ B ) e. Fin )
3		difinf	|- ( ( -. A e. Fin /\ B e. Fin ) -> -. ( A \ B ) e. Fin )
4	3	ancoms	|- ( ( B e. Fin /\ -. A e. Fin ) -> -. ( A \ B ) e. Fin )
5	4	ex	|- ( B e. Fin -> ( -. A e. Fin -> -. ( A \ B ) e. Fin ) )
6	5	con4d	|- ( B e. Fin -> ( ( A \ B ) e. Fin -> A e. Fin ) )
7	6	imp	|- ( ( B e. Fin /\ ( A \ B ) e. Fin ) -> A e. Fin )
8	2 7	impbida	|- ( B e. Fin -> ( A e. Fin <-> ( A \ B ) e. Fin ) )