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 3107 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
2 | 1 | simplbi 272 | 1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1331 ⊆ wss 3066 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-in 3072 df-ss 3079 |
This theorem is referenced by: eqimss2 3147 uneqin 3322 sssnr 3675 sssnm 3676 ssprr 3678 sstpr 3679 snsspw 3686 pwpwssunieq 3896 elpwuni 3897 disjeq2 3905 disjeq1 3908 pwne 4079 pwssunim 4201 poeq2 4217 seeq1 4256 seeq2 4257 trsucss 4340 onsucelsucr 4419 xp11m 4972 funeq 5138 fnresdm 5227 fssxp 5285 ffdm 5288 fcoi1 5298 fof 5340 dff1o2 5365 fvmptss2 5489 fvmptssdm 5498 fprg 5596 dff1o6 5670 tposeq 6137 nntri1 6385 nntri2or2 6387 nnsseleq 6390 infnninf 7015 frec2uzf1od 10172 hashinfuni 10516 setsresg 11986 setsslid 11998 strle1g 12038 cncnpi 12386 hmeores 12473 limcimolemlt 12791 recnprss 12814 el2oss1o 13177 0nninf 13186 nninfall 13193 |
Copyright terms: Public domain | W3C validator |