Theorem difsnpss

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)

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

Proof

Step	Hyp	Ref	Expression
1		notnotb	|- ( A e. B <-> -. -. A e. B )
2		difss	|- ( B \ { A } ) C_ B
3	2	biantrur	|- ( ( B \ { A } ) =/= B <-> ( ( B \ { A } ) C_ B /\ ( B \ { A } ) =/= B ) )
4		difsnb	|- ( -. A e. B <-> ( B \ { A } ) = B )
5	4	necon3bbii	|- ( -. -. A e. B <-> ( B \ { A } ) =/= B )
6		df-pss	|- ( ( B \ { A } ) C. B <-> ( ( B \ { A } ) C_ B /\ ( B \ { A } ) =/= B ) )
7	3 5 6	3bitr4i	|- ( -. -. A e. B <-> ( B \ { A } ) C. B )
8	1 7	bitri	|- ( A e. B <-> ( B \ { A } ) C. B )