![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqimss | 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 | ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqss 3054 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
2 | 1 | simplbi 269 | 1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1296 ⊆ wss 3013 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-11 1449 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-in 3019 df-ss 3026 |
This theorem is referenced by: eqimss2 3094 uneqin 3266 sssnr 3619 sssnm 3620 ssprr 3622 sstpr 3623 snsspw 3630 pwpwssunieq 3839 elpwuni 3840 disjeq2 3848 disjeq1 3851 pwne 4016 pwssunim 4135 poeq2 4151 seeq1 4190 seeq2 4191 trsucss 4274 onsucelsucr 4353 xp11m 4903 funeq 5069 fnresdm 5157 fssxp 5213 ffdm 5216 fcoi1 5226 fof 5268 dff1o2 5293 fvmptss2 5414 fvmptssdm 5423 fprg 5519 dff1o6 5593 tposeq 6050 nntri1 6297 nntri2or2 6299 nnsseleq 6302 infnninf 6893 frec2uzf1od 9962 hashinfuni 10316 setsresg 11697 setsslid 11709 strle1g 11749 cncnpi 12095 el2oss1o 12609 0nninf 12614 nninfall 12621 |
Copyright terms: Public domain | W3C validator |