This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )