Theorem sspss 4034

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

Assertion

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

Proof of Theorem sspss

Step	Hyp	Ref	Expression
1		dfpss2 4020	. . . . 5 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
2	1	simplbi2 501	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 → 𝐴 ⊊ 𝐵))
3	2	con1d 145	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 ⊊ 𝐵 → 𝐴 = 𝐵))
4	3	orrd 869	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵))
5		pssss 4030	. . 3 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)
6		eqimss 3973	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
7	5, 6	jaoi 863	. 2 ⊢ ((𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵) → 𝐴 ⊆ 𝐵)
8	4, 7	impbii 210	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 207   ∨ wo 853   = wceq 1547   ⊆ wss 3883   ⊊ wpss 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-cleq 2731  df-ne 2935  df-ss 3900  df-pss 3903

This theorem is referenced by:  sspsstri  4037  sspsstr  4040  psssstr  4041  ordsseleq  6340  sorpssuni  7676  sorpssint  7677  ssnnfi  9095  ackbij1b  10152  fin23lem40  10265  zorng  10418  psslinpr  10946  suplem2pr  10968  ressval3d  17208  mrissmrcd  17598  pgpssslw  19581  pgpfac1lem5  20048  idnghm  24727  leslss  27920  dfon2lem4  36021  finminlem  36555  lkrss2N  39670  dvh3dim3N  41950  ordsssucb  43789