Theorem sspss 4125

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∨ wo 846   = wceq 1537   ⊆ wss 3976   ⊊ wpss 3977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-cleq 2732  df-ne 2947  df-ss 3993  df-pss 3996

This theorem is referenced by:  sspsstri  4128  sspsstr  4131  psssstr  4132  ordsseleq  6424  sorpssuni  7767  sorpssint  7768  ssnnfi  9235  ssnnfiOLD  9236  ackbij1b  10307  fin23lem40  10420  zorng  10573  psslinpr  11100  suplem2pr  11122  ressval3d  17305  ressval3dOLD  17306  mrissmrcd  17698  pgpssslw  19656  pgpfac1lem5  20123  idnghm  24785  slelss  27964  dfon2lem4  35750  finminlem  36284  lkrss2N  39125  dvh3dim3N  41406  ordsssucb  43297