Theorem sspss

Description: Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996)

	Ref	Expression
Assertion	sspss	|- ( A C_ B <-> ( A C. B \/ A = B ) )

Proof

Step	Hyp	Ref	Expression
1		dfpss2	|- ( A C. B <-> ( A C_ B /\ -. A = B ) )
2	1	simplbi2	|- ( A C_ B -> ( -. A = B -> A C. B ) )
3	2	con1d	|- ( A C_ B -> ( -. A C. B -> A = B ) )
4	3	orrd	|- ( A C_ B -> ( A C. B \/ A = B ) )
5		pssss	|- ( A C. B -> A C_ B )
6		eqimss	|- ( A = B -> A C_ B )
7	5 6	jaoi	|- ( ( A C. B \/ A = B ) -> A C_ B )
8	4 7	impbii	|- ( A C_ B <-> ( A C. B \/ A = B ) )