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 4065 | . . . . 5 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | |
2 | 1 | simplbi2 503 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 → 𝐴 ⊊ 𝐵)) |
3 | 2 | con1d 147 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 ⊊ 𝐵 → 𝐴 = 𝐵)) |
4 | 3 | orrd 859 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) |
5 | pssss 4075 | . . 3 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | |
6 | eqimss 4026 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
7 | 5, 6 | jaoi 853 | . 2 ⊢ ((𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵) → 𝐴 ⊆ 𝐵) |
8 | 4, 7 | impbii 211 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 208 ∨ wo 843 = wceq 1536 ⊆ wss 3939 ⊊ wpss 3940 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-ne 3020 df-in 3946 df-ss 3955 df-pss 3957 |
This theorem is referenced by: sspsstri 4082 sspsstr 4085 psssstr 4086 ordsseleq 6223 sorpssuni 7461 sorpssint 7462 ssnnfi 8740 ackbij1b 9664 fin23lem40 9776 zorng 9929 psslinpr 10456 suplem2pr 10478 ressval3d 16564 mrissmrcd 16914 pgpssslw 18742 pgpfac1lem5 19204 idnghm 23355 dfon2lem4 33035 finminlem 33670 lkrss2N 36309 dvh3dim3N 38589 |
Copyright terms: Public domain | W3C validator |