![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqimss2i | Structured version Visualization version GIF version |
Description: Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.) |
Ref | Expression |
---|---|
eqimssi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
eqimss2i | ⊢ 𝐵 ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 3848 | . 2 ⊢ 𝐵 ⊆ 𝐵 | |
2 | eqimssi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
3 | 1, 2 | sseqtr4i 3863 | 1 ⊢ 𝐵 ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1656 ⊆ wss 3798 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-in 3805 df-ss 3812 |
This theorem is referenced by: cotr3 14103 supcvg 14969 prodfclim1 15005 ef0lem 15188 1strbas 16346 restid 16454 cayley 18191 gsumval3 18668 gsumzaddlem 18681 kgencn3 21739 hmeores 21952 opnfbas 22023 tsmsf1o 22325 ust0 22400 icchmeo 23117 plyeq0lem 24372 ulmdvlem1 24560 basellem7 25233 basellem9 25235 dchrisumlem3 25600 structvtxvallem 26325 struct2griedg 26333 ivthALT 32863 aomclem4 38469 hashnzfzclim 39360 binomcxplemrat 39388 climsuselem1 40632 |
Copyright terms: Public domain | W3C validator |