![]() |
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 4002 | . 2 ⊢ 𝐴 ⊆ 𝐴 | |
2 | eqimssi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
3 | 1, 2 | sseqtri 4016 | 1 ⊢ 𝐴 ⊆ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ⊆ wss 3947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3473 df-in 3954 df-ss 3964 |
This theorem is referenced by: funi 6585 fpr 7163 tz7.48-2 8463 trcl 9752 zorn2lem4 10523 zmin 12959 elfzo1 13715 om2uzf1oi 13951 0trrel 14961 sumsplit 15747 isumless 15824 rnglidl1 21128 frlmip 21712 ust0 24137 rrxprds 25330 rrxip 25331 ovoliunnul 25449 vitalilem5 25554 logtayl 26607 nbgr2vtx1edg 29176 nbuhgr2vtx1edgb 29178 mayetes3i 31552 cycpmconjslem2 32889 eulerpartlemsv2 33978 eulerpartlemsv3 33981 eulerpartlemv 33984 eulerpartlemb 33988 poimirlem9 37102 dvasin 37177 dmcoss3 37925 disjALTVid 38227 sticksstones17 41635 sticksstones18 41636 nna4b4nsq 42084 cnvrcl0 43055 corclrcl 43137 trclrelexplem 43141 cotrcltrcl 43155 he0 43214 dvsid 43768 binomcxplemnotnn0 43793 fourierdlem62 45556 fourierdlem66 45560 |
Copyright terms: Public domain | W3C validator |