![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqimssi | Structured version Visualization version GIF version |
Description: Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.) |
Ref | Expression |
---|---|
eqimssi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
eqimssi | ⊢ 𝐴 ⊆ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 4018 | . 2 ⊢ 𝐴 ⊆ 𝐴 | |
2 | eqimssi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
3 | 1, 2 | sseqtri 4032 | 1 ⊢ 𝐴 ⊆ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ⊆ wss 3963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-cleq 2727 df-ss 3980 |
This theorem is referenced by: funi 6600 fpr 7174 tz7.48-2 8481 trcl 9766 zorn2lem4 10537 zmin 12984 elfzo1 13749 om2uzf1oi 13991 0trrel 15017 sumsplit 15801 isumless 15878 rnglidl1 21260 frlmip 21816 ust0 24244 rrxprds 25437 rrxip 25438 ovoliunnul 25556 vitalilem5 25661 logtayl 26717 nbgr2vtx1edg 29382 nbuhgr2vtx1edgb 29384 mayetes3i 31758 cycpmconjslem2 33158 eulerpartlemsv2 34340 eulerpartlemsv3 34343 eulerpartlemv 34346 eulerpartlemb 34350 poimirlem9 37616 dvasin 37691 dmcoss3 38435 disjALTVid 38737 sticksstones17 42145 sticksstones18 42146 nna4b4nsq 42647 cnvrcl0 43615 corclrcl 43697 trclrelexplem 43701 cotrcltrcl 43715 he0 43774 dvsid 44327 binomcxplemnotnn0 44352 fourierdlem62 46124 fourierdlem66 46128 isubgr3stgrlem6 47874 |
Copyright terms: Public domain | W3C validator |