|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > sspss | Structured version Visualization version GIF version | ||
| Description: Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.) | 
| Ref | Expression | 
|---|---|
| sspss | ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | dfpss2 4087 | . . . . 5 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | |
| 2 | 1 | simplbi2 500 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 → 𝐴 ⊊ 𝐵)) | 
| 3 | 2 | con1d 145 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 ⊊ 𝐵 → 𝐴 = 𝐵)) | 
| 4 | 3 | orrd 863 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) | 
| 5 | pssss 4097 | . . 3 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | |
| 6 | eqimss 4041 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
| 7 | 5, 6 | jaoi 857 | . 2 ⊢ ((𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵) → 𝐴 ⊆ 𝐵) | 
| 8 | 4, 7 | impbii 209 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 ↔ wb 206 ∨ wo 847 = wceq 1539 ⊆ wss 3950 ⊊ wpss 3951 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1779 df-cleq 2728 df-ne 2940 df-ss 3967 df-pss 3970 | 
| This theorem is referenced by: sspsstri 4104 sspsstr 4107 psssstr 4108 ordsseleq 6412 sorpssuni 7753 sorpssint 7754 ssnnfi 9210 ackbij1b 10279 fin23lem40 10392 zorng 10545 psslinpr 11072 suplem2pr 11094 ressval3d 17293 mrissmrcd 17684 pgpssslw 19633 pgpfac1lem5 20100 idnghm 24765 slelss 27947 dfon2lem4 35788 finminlem 36320 lkrss2N 39171 dvh3dim3N 41452 ordsssucb 43353 | 
| Copyright terms: Public domain | W3C validator |