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 3923 | . 2 ⊢ 𝐴 ⊆ 𝐴 | |
2 | eqimssi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
3 | 1, 2 | sseqtri 3937 | 1 ⊢ 𝐴 ⊆ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ⊆ wss 3866 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-in 3873 df-ss 3883 |
This theorem is referenced by: funi 6412 fpr 6969 tz7.48-2 8178 trcl 9344 zorn2lem4 10113 zmin 12540 elfzo1 13292 om2uzf1oi 13526 0trrel 14544 sumsplit 15332 isumless 15409 frlmip 20740 ust0 23117 rrxprds 24286 rrxip 24287 ovoliunnul 24404 vitalilem5 24509 logtayl 25548 nbgr2vtx1edg 27438 nbuhgr2vtx1edgb 27440 mayetes3i 29810 cycpmconjslem2 31141 eulerpartlemsv2 32037 eulerpartlemsv3 32040 eulerpartlemv 32043 eulerpartlemb 32047 poimirlem9 35523 dvasin 35598 dmcoss3 36308 disjALTVid 36600 sticksstones17 39841 sticksstones18 39842 nna4b4nsq 40200 cnvrcl0 40909 corclrcl 40992 trclrelexplem 40996 cotrcltrcl 41010 he0 41069 dvsid 41622 binomcxplemnotnn0 41647 fourierdlem62 43384 fourierdlem66 43388 |
Copyright terms: Public domain | W3C validator |