![]() |
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 4002 | . 2 ⊢ 𝐵 ⊆ 𝐵 | |
2 | eqimssi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
3 | 1, 2 | sseqtrri 4017 | 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-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-ss 3964 |
This theorem is referenced by: cotr3 14983 supcvg 15860 prodfclim1 15897 ef0lem 16080 1strbas 17230 1strbasOLD 17231 restid 17448 cayley 19412 gsumval3 19905 gsumzaddlem 19919 kgencn3 23553 hmeores 23766 opnfbas 23837 tsmsf1o 24140 ust0 24215 icchmeo 24956 icchmeoOLD 24957 plyeq0lem 26237 ulmdvlem1 26429 basellem7 27115 basellem9 27117 dchrisumlem3 27520 structvtxvallem 28956 struct2griedg 28964 gsumhashmul 32925 cycpmfvlem 32990 cycpmfv3 32993 constr01 33600 ivthALT 36047 aomclem4 42718 hashnzfzclim 43996 binomcxplemrat 44024 climsuselem1 45228 gsumfsupp 47559 |
Copyright terms: Public domain | W3C validator |