![]() |
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 4050 | . . . . 5 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | |
2 | 1 | simplbi2 502 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 → 𝐴 ⊊ 𝐵)) |
3 | 2 | con1d 145 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 ⊊ 𝐵 → 𝐴 = 𝐵)) |
4 | 3 | orrd 862 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) |
5 | pssss 4060 | . . 3 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | |
6 | eqimss 4005 | . . 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 3915 ⊊ wpss 3916 |
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 2708 |
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 2715 df-cleq 2729 df-clel 2815 df-ne 2945 df-v 3450 df-in 3922 df-ss 3932 df-pss 3934 |
This theorem is referenced by: sspsstri 4067 sspsstr 4070 psssstr 4071 ordsseleq 6351 sorpssuni 7674 sorpssint 7675 ssnnfi 9120 ssnnfiOLD 9121 ackbij1b 10182 fin23lem40 10294 zorng 10447 psslinpr 10974 suplem2pr 10996 ressval3d 17134 ressval3dOLD 17135 mrissmrcd 17527 pgpssslw 19403 pgpfac1lem5 19865 idnghm 24123 dfon2lem4 34400 finminlem 34819 lkrss2N 37660 dvh3dim3N 39941 |
Copyright terms: Public domain | W3C validator |