Metamath Proof Explorer


Theorem nsspssun

Description: Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004)

Ref Expression
Assertion nsspssun ( ¬ 𝐴𝐵𝐵 ⊊ ( 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 ssun2 𝐵 ⊆ ( 𝐴𝐵 )
2 1 biantrur ( ¬ ( 𝐴𝐵 ) ⊆ 𝐵 ↔ ( 𝐵 ⊆ ( 𝐴𝐵 ) ∧ ¬ ( 𝐴𝐵 ) ⊆ 𝐵 ) )
3 ssid 𝐵𝐵
4 3 biantru ( 𝐴𝐵 ↔ ( 𝐴𝐵𝐵𝐵 ) )
5 unss ( ( 𝐴𝐵𝐵𝐵 ) ↔ ( 𝐴𝐵 ) ⊆ 𝐵 )
6 4 5 bitri ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) ⊆ 𝐵 )
7 2 6 xchnxbir ( ¬ 𝐴𝐵 ↔ ( 𝐵 ⊆ ( 𝐴𝐵 ) ∧ ¬ ( 𝐴𝐵 ) ⊆ 𝐵 ) )
8 dfpss3 ( 𝐵 ⊊ ( 𝐴𝐵 ) ↔ ( 𝐵 ⊆ ( 𝐴𝐵 ) ∧ ¬ ( 𝐴𝐵 ) ⊆ 𝐵 ) )
9 7 8 bitr4i ( ¬ 𝐴𝐵𝐵 ⊊ ( 𝐴𝐵 ) )