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

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 ( 𝐴 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝐴 ) ) = 𝐴 )

Proof

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