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 3986 | . 2 ⊢ 𝐵 ⊆ 𝐵 | |
2 | eqimssi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
3 | 1, 2 | sseqtrri 4001 | 1 ⊢ 𝐵 ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-in 3940 df-ss 3949 |
This theorem is referenced by: cotr3 14326 supcvg 15199 prodfclim1 15237 ef0lem 15420 1strbas 16587 restid 16695 cayley 18471 gsumval3 18956 gsumzaddlem 18970 kgencn3 22094 hmeores 22307 opnfbas 22378 tsmsf1o 22680 ust0 22755 icchmeo 23472 plyeq0lem 24727 ulmdvlem1 24915 basellem7 25591 basellem9 25593 dchrisumlem3 25994 structvtxvallem 26732 struct2griedg 26740 cycpmfvlem 30681 cycpmfv3 30684 ivthALT 33580 aomclem4 39535 hashnzfzclim 40531 binomcxplemrat 40559 climsuselem1 41764 gsumfsupp 43966 |
Copyright terms: Public domain | W3C validator |