Theorem diffib

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

	Ref	Expression
Assertion	diffib	⊢ ( 𝐵 ∈ Fin → ( 𝐴 ∈ Fin ↔ ( 𝐴 ∖ 𝐵 ) ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		diffi	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ 𝐵 ) ∈ Fin )
2	1	adantl	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( 𝐴 ∖ 𝐵 ) ∈ Fin )
3		difinf	⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ¬ ( 𝐴 ∖ 𝐵 ) ∈ Fin )
4	3	ancoms	⊢ ( ( 𝐵 ∈ Fin ∧ ¬ 𝐴 ∈ Fin ) → ¬ ( 𝐴 ∖ 𝐵 ) ∈ Fin )
5	4	ex	⊢ ( 𝐵 ∈ Fin → ( ¬ 𝐴 ∈ Fin → ¬ ( 𝐴 ∖ 𝐵 ) ∈ Fin ) )
6	5	con4d	⊢ ( 𝐵 ∈ Fin → ( ( 𝐴 ∖ 𝐵 ) ∈ Fin → 𝐴 ∈ Fin ) )
7	6	imp	⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝐴 ∖ 𝐵 ) ∈ Fin ) → 𝐴 ∈ Fin )
8	2 7	impbida	⊢ ( 𝐵 ∈ Fin → ( 𝐴 ∈ Fin ↔ ( 𝐴 ∖ 𝐵 ) ∈ Fin ) )