Metamath Proof Explorer

Theorem diffib

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

Ref Expression
Assertion diffib ⊢ B ∈ Fin → A ∈ Fin ↔ A ∖ B ∈ Fin

Proof

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