Theorem sspss 4065

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 4051	. . . . 5 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
2	1	simplbi2 500	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 → 𝐴 ⊊ 𝐵))
3	2	con1d 145	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 ⊊ 𝐵 → 𝐴 = 𝐵))
4	3	orrd 863	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵))
5		pssss 4061	. . 3 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)
6		eqimss 4005	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
7	5, 6	jaoi 857	. 2 ⊢ ((𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵) → 𝐴 ⊆ 𝐵)
8	4, 7	impbii 209	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∨ wo 847   = wceq 1540   ⊆ wss 3914   ⊊ wpss 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-cleq 2721  df-ne 2926  df-ss 3931  df-pss 3934

This theorem is referenced by:  sspsstri  4068  sspsstr  4071  psssstr  4072  ordsseleq  6361  sorpssuni  7708  sorpssint  7709  ssnnfi  9133  ackbij1b  10191  fin23lem40  10304  zorng  10457  psslinpr  10984  suplem2pr  11006  ressval3d  17216  mrissmrcd  17601  pgpssslw  19544  pgpfac1lem5  20011  idnghm  24631  slelss  27820  dfon2lem4  35774  finminlem  36306  lkrss2N  39162  dvh3dim3N  41443  ordsssucb  43324