Theorem sspss 4064

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 4050	. . . . 5 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
2	1	simplbi2 505	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 → 𝐴 ⊊ 𝐵))
3	2	con1d 146	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 ⊊ 𝐵 → 𝐴 = 𝐵))
4	3	orrd 876	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵))
5		pssss 4060	. . 3 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)
6		eqimss 4003	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
7	5, 6	jaoi 870	. 2 ⊢ ((𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵) → 𝐴 ⊆ 𝐵)
8	4, 7	impbii 212	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∨ wo 860   = wceq 1567   ⊆ wss 3913   ⊊ wpss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-cleq 2761  df-ne 2965  df-ss 3930  df-pss 3933

This theorem is referenced by:  sspsstri  4068  sspsstr  4071  psssstr  4072  ordsseleq  6391  sorpssuni  7730  sorpssint  7731  ssnnfi  9154  ackbij1b  10221  fin23lem40  10335  zorng  10488  psslinpr  11016  suplem2pr  11038  ressval3d  17306  mrissmrcd  17696  pgpssslw  19684  pgpfac1lem5  20151  idnghm  24869  leslss  28068  dfon2lem4  36209  finminlem  36752  lkrss2N  39867  dvh3dim3N  42147  ordsssucb  43988