Theorem sspss

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

	Ref	Expression
Assertion	sspss	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dfpss2	⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) )
2	1	simplbi2	⊢ ( 𝐴 ⊆ 𝐵 → ( ¬ 𝐴 = 𝐵 → 𝐴 ⊊ 𝐵 ) )
3	2	con1d	⊢ ( 𝐴 ⊆ 𝐵 → ( ¬ 𝐴 ⊊ 𝐵 → 𝐴 = 𝐵 ) )
4	3	orrd	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) )
5		pssss	⊢ ( 𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵 )
6		eqimss	⊢ ( 𝐴 = 𝐵 → 𝐴 ⊆ 𝐵 )
7	5 6	jaoi	⊢ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) → 𝐴 ⊆ 𝐵 )
8	4 7	impbii	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) )