Metamath Proof Explorer

Theorem dfss4

Description: Subclass defined in terms of class difference. See comments under dfun2 . (Contributed by NM, 22-Mar-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion dfss4 ⊢ A ⊆ B ↔ B ∖ B ∖ A = A

Proof

Step Hyp Ref Expression
1 sseqin2 ⊢ A ⊆ B ↔ B ∩ A = A
2 eldif ⊢ x ∈ B ∖ A ↔ x ∈ B ∧ ¬ x ∈ A
3 2 notbii ⊢ ¬ x ∈ B ∖ A ↔ ¬ x ∈ B ∧ ¬ x ∈ A
4 3 anbi2i ⊢ x ∈ B ∧ ¬ x ∈ B ∖ A ↔ x ∈ B ∧ ¬ x ∈ B ∧ ¬ x ∈ A
5 elin ⊢ x ∈ B ∩ A ↔ x ∈ B ∧ x ∈ A
6 abai ⊢ x ∈ B ∧ x ∈ A ↔ x ∈ B ∧ x ∈ B → x ∈ A
7 iman ⊢ x ∈ B → x ∈ A ↔ ¬ x ∈ B ∧ ¬ x ∈ A
8 7 anbi2i ⊢ x ∈ B ∧ x ∈ B → x ∈ A ↔ x ∈ B ∧ ¬ x ∈ B ∧ ¬ x ∈ A
9 5 6 8 3bitri ⊢ x ∈ B ∩ A ↔ x ∈ B ∧ ¬ x ∈ B ∧ ¬ x ∈ A
10 4 9 bitr4i ⊢ x ∈ B ∧ ¬ x ∈ B ∖ A ↔ x ∈ B ∩ A
11 10 difeqri ⊢ B ∖ B ∖ A = B ∩ A
12 11 eqeq1i ⊢ B ∖ B ∖ A = A ↔ B ∩ A = A
13 1 12 bitr4i ⊢ A ⊆ B ↔ B ∖ B ∖ A = A