![]() |
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 4085 | . . . . 5 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | |
2 | 1 | simplbi2 501 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 → 𝐴 ⊊ 𝐵)) |
3 | 2 | con1d 145 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 ⊊ 𝐵 → 𝐴 = 𝐵)) |
4 | 3 | orrd 861 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) |
5 | pssss 4095 | . . 3 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | |
6 | eqimss 4040 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
7 | 5, 6 | jaoi 855 | . 2 ⊢ ((𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵) → 𝐴 ⊆ 𝐵) |
8 | 4, 7 | impbii 208 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∨ wo 845 = wceq 1541 ⊆ wss 3948 ⊊ wpss 3949 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ne 2941 df-v 3476 df-in 3955 df-ss 3965 df-pss 3967 |
This theorem is referenced by: sspsstri 4102 sspsstr 4105 psssstr 4106 ordsseleq 6393 sorpssuni 7721 sorpssint 7722 ssnnfi 9168 ssnnfiOLD 9169 ackbij1b 10233 fin23lem40 10345 zorng 10498 psslinpr 11025 suplem2pr 11047 ressval3d 17190 ressval3dOLD 17191 mrissmrcd 17583 pgpssslw 19481 pgpfac1lem5 19948 idnghm 24259 dfon2lem4 34753 finminlem 35198 lkrss2N 38034 dvh3dim3N 40315 ordsssucb 42075 |
Copyright terms: Public domain | W3C validator |