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

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 
|- ( -. A C_ B <-> B C. ( A u. B ) )

Proof

Step Hyp Ref Expression
1 ssun2 
 |-  B C_ ( A u. B )
2 1 biantrur 
 |-  ( -. ( A u. B ) C_ B <-> ( B C_ ( A u. B ) /\ -. ( A u. B ) C_ B ) )
3 ssid 
 |-  B C_ B
4 3 biantru 
 |-  ( A C_ B <-> ( A C_ B /\ B C_ B ) )
5 unss 
 |-  ( ( A C_ B /\ B C_ B ) <-> ( A u. B ) C_ B )
6 4 5 bitri 
 |-  ( A C_ B <-> ( A u. B ) C_ B )
7 2 6 xchnxbir 
 |-  ( -. A C_ B <-> ( B C_ ( A u. B ) /\ -. ( A u. B ) C_ B ) )
8 dfpss3 
 |-  ( B C. ( A u. B ) <-> ( B C_ ( A u. B ) /\ -. ( A u. B ) C_ B ) )
9 7 8 bitr4i 
 |-  ( -. A C_ B <-> B C. ( A u. B ) )