![]() |
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 4086 | . . . . 5 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | |
2 | 1 | simplbi2 502 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 → 𝐴 ⊊ 𝐵)) |
3 | 2 | con1d 145 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 ⊊ 𝐵 → 𝐴 = 𝐵)) |
4 | 3 | orrd 862 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) |
5 | pssss 4096 | . . 3 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | |
6 | eqimss 4041 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
7 | 5, 6 | jaoi 856 | . 2 ⊢ ((𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵) → 𝐴 ⊆ 𝐵) |
8 | 4, 7 | impbii 208 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∨ wo 846 = wceq 1542 ⊆ wss 3949 ⊊ wpss 3950 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-v 3477 df-in 3956 df-ss 3966 df-pss 3968 |
This theorem is referenced by: sspsstri 4103 sspsstr 4106 psssstr 4107 ordsseleq 6394 sorpssuni 7722 sorpssint 7723 ssnnfi 9169 ssnnfiOLD 9170 ackbij1b 10234 fin23lem40 10346 zorng 10499 psslinpr 11026 suplem2pr 11048 ressval3d 17191 ressval3dOLD 17192 mrissmrcd 17584 pgpssslw 19482 pgpfac1lem5 19949 idnghm 24260 dfon2lem4 34758 finminlem 35203 lkrss2N 38039 dvh3dim3N 40320 ordsssucb 42085 |
Copyright terms: Public domain | W3C validator |