![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > ILE Home > Th. List > eqimss | Structured version GIF version |
Description: Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
Ref | Expression |
---|---|
eqimss | ⊢ (A = B → A ⊆ B) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqss 2936 | . 2 ⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A)) | |
2 | 1 | simplbi 259 | 1 ⊢ (A = B → A ⊆ B) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1228 ⊆ wss 2893 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1316 ax-7 1317 ax-gen 1318 ax-ie1 1364 ax-ie2 1365 ax-8 1377 ax-11 1379 ax-4 1382 ax-17 1401 ax-i9 1405 ax-ial 1410 ax-i5r 1411 ax-ext 2005 |
This theorem depends on definitions: df-bi 110 df-nf 1330 df-sb 1629 df-clab 2010 df-cleq 2016 df-clel 2019 df-in 2900 df-ss 2907 |
This theorem is referenced by: eqimss2 2974 sspssr 3019 sspsstrir 3022 uneqin 3164 sssnr 3497 sssnm 3498 ssprr 3500 sstpr 3501 snsspw 3508 elpwuni 3714 disjeq2 3722 disjeq1 3725 pwne 3886 pwssunim 3994 poeq2 4010 seeq1 4042 seeq2 4043 trsucss 4108 onsucelsucr 4181 xp11m 4684 funeq 4845 fnresdm 4932 fssxp 4981 ffdm 4984 fcoi1 4993 fof 5029 dff1o2 5054 fvmptss2 5170 fvmptssdm 5178 fprg 5269 dff1o6 5339 tposeq 5781 nntri1 5984 |
Copyright terms: Public domain | W3C validator |