![]() |
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 3910 | . 2 ⊢ 𝐴 ⊆ 𝐴 | |
2 | eqimssi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
3 | 1, 2 | sseqtri 3924 | 1 ⊢ 𝐴 ⊆ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ⊆ wss 3859 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-in 3866 df-ss 3874 |
This theorem is referenced by: funi 6257 fpr 6779 tz7.48-2 7929 trcl 9016 zorn2lem4 9767 zmin 12193 elfzo1 12937 om2uzf1oi 13171 0trrel 14175 sumsplit 14956 isumless 15033 frlmip 20604 ust0 22511 rrxprds 23675 rrxip 23676 ovoliunnul 23791 vitalilem5 23896 logtayl 24924 nbgr2vtx1edg 26815 nbuhgr2vtx1edgb 26817 mayetes3i 29197 cycpmconjslem2 30435 eulerpartlemsv2 31233 eulerpartlemsv3 31236 eulerpartlemv 31239 eulerpartlemb 31243 poimirlem9 34432 dvasin 34509 dmcoss3 35224 disjALTVid 35516 cnvrcl0 39470 corclrcl 39537 trclrelexplem 39541 cotrcltrcl 39555 he0 39615 dvsid 40201 binomcxplemnotnn0 40226 fourierdlem62 41995 fourierdlem66 41999 |
Copyright terms: Public domain | W3C validator |