![]() |
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 4013 | . . . . 5 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | |
2 | 1 | simplbi2 504 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 → 𝐴 ⊊ 𝐵)) |
3 | 2 | con1d 147 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 ⊊ 𝐵 → 𝐴 = 𝐵)) |
4 | 3 | orrd 860 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) |
5 | pssss 4023 | . . 3 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | |
6 | eqimss 3971 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
7 | 5, 6 | jaoi 854 | . 2 ⊢ ((𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵) → 𝐴 ⊆ 𝐵) |
8 | 4, 7 | impbii 212 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 ∨ wo 844 = wceq 1538 ⊆ wss 3881 ⊊ wpss 3882 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-ne 2988 df-v 3443 df-in 3888 df-ss 3898 df-pss 3900 |
This theorem is referenced by: sspsstri 4030 sspsstr 4033 psssstr 4034 ordsseleq 6188 sorpssuni 7438 sorpssint 7439 ssnnfi 8721 ackbij1b 9650 fin23lem40 9762 zorng 9915 psslinpr 10442 suplem2pr 10464 ressval3d 16553 mrissmrcd 16903 pgpssslw 18731 pgpfac1lem5 19194 idnghm 23349 dfon2lem4 33144 finminlem 33779 lkrss2N 36465 dvh3dim3N 38745 |
Copyright terms: Public domain | W3C validator |