![]() |
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 3170 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
2 | 1 | simplbi 274 | 1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 ⊆ wss 3129 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 |
This theorem is referenced by: eqimss2 3210 uneqin 3386 sssnr 3753 sssnm 3754 ssprr 3756 sstpr 3757 snsspw 3764 pwpwssunieq 3975 elpwuni 3976 disjeq2 3984 disjeq1 3987 pwne 4160 pwssunim 4284 poeq2 4300 seeq1 4339 seeq2 4340 trsucss 4423 onsucelsucr 4507 xp11m 5067 funeq 5236 fnresdm 5325 fssxp 5383 ffdm 5386 fcoi1 5396 fof 5438 dff1o2 5466 fvmptss2 5591 fvmptssdm 5600 fprg 5699 dff1o6 5776 tposeq 6247 el2oss1o 6443 nntri1 6496 nntri2or2 6498 nnsseleq 6501 infnninf 7121 infnninfOLD 7122 nninfwlpoimlemg 7172 exmidontri2or 7241 frec2uzf1od 10405 hashinfuni 10756 setsresg 12499 setsslid 12512 strle1g 12564 cncnpi 13698 hmeores 13785 limcimolemlt 14103 recnprss 14126 0nninf 14723 nninfall 14728 |
Copyright terms: Public domain | W3C validator |