|   | 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 4005 | . 2 ⊢ 𝐴 ⊆ 𝐴 | |
| 2 | eqimssi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
| 3 | 1, 2 | sseqtri 4031 | 1 ⊢ 𝐴 ⊆ 𝐵 | 
| Colors of variables: wff setvar class | 
| Syntax hints: = wceq 1539 ⊆ wss 3950 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-ss 3967 | 
| This theorem is referenced by: funi 6597 fpr 7173 tz7.48-2 8483 trcl 9769 zorn2lem4 10540 zmin 12987 elfzo1 13753 om2uzf1oi 13995 0trrel 15021 sumsplit 15805 isumless 15882 rnglidl1 21243 frlmip 21799 ust0 24229 rrxprds 25424 rrxip 25425 ovoliunnul 25543 vitalilem5 25648 logtayl 26703 nbgr2vtx1edg 29368 nbuhgr2vtx1edgb 29370 mayetes3i 31749 cycpmconjslem2 33176 eulerpartlemsv2 34361 eulerpartlemsv3 34364 eulerpartlemv 34367 eulerpartlemb 34371 poimirlem9 37637 dvasin 37712 dmcoss3 38455 disjALTVid 38757 sticksstones17 42165 sticksstones18 42166 nna4b4nsq 42675 cnvrcl0 43643 corclrcl 43725 trclrelexplem 43729 cotrcltrcl 43743 he0 43802 dvsid 44355 binomcxplemnotnn0 44380 wfaxreg 45022 fourierdlem62 46188 fourierdlem66 46192 isubgr3stgrlem6 47943 | 
| Copyright terms: Public domain | W3C validator |