Theorem difsnpss 4159

Description: ( B \ { A } ) is a proper subclass of B if and only if A is a member of B. (Contributed by David Moews, 1-May-2017.)

Assertion

Ref	Expression
difsnpss	|- ( A e. B <-> ( B \ { A } ) C. B )

Proof of Theorem difsnpss

Step	Hyp	Ref	Expression
1		notnot 289	. 2 |- ( A e. B <-> -. -. A e. B )
2		difss 3617	. . . 4 |- ( B \ { A } ) C_ B
3	2	biantrur 504	. . 3 |- ( ( B \ { A } ) =/= B <-> ( ( B \ { A } ) C_ B /\ ( B \ { A } ) =/= B ) )
4		difsnb 4158	. . . 4 |- ( -. A e. B <-> ( B \ { A } ) = B )
5	4	necon3bbii 2715	. . 3 |- ( -. -. A e. B <-> ( B \ { A } ) =/= B )
6		df-pss 3477	. . 3 |- ( ( B \ { A } ) C. B <-> ( ( B \ { A } ) C_ B /\ ( B \ { A } ) =/= B ) )
7	3, 5, 6	3bitr4i 277	. 2 |- ( -. -. A e. B <-> ( B \ { A } ) C. B )
8	1, 7	bitri 249	1 |- ( A e. B <-> ( B \ { A } ) C. B )

Syntax hints:   -. wn 3   <-> wb 184   /\ wa 367   e. wcel 1823   =/= wne 2649   \ cdif 3458   C_ wss 3461   C. wpss 3462   {csn 4016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-in 3468  df-ss 3475  df-pss 3477  df-sn 4017

This theorem is referenced by:  marypha1lem  7885  infpss  8588  ominf4  8683  mrieqv2d  15131