| 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 4006 | . 2 ⊢ 𝐵 ⊆ 𝐵 | |
| 2 | eqimssi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
| 3 | 1, 2 | sseqtrri 4033 | 1 ⊢ 𝐵 ⊆ 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 |
| This theorem is referenced by: cotr3 15017 supcvg 15892 prodfclim1 15929 ef0lem 16114 1strbas 17263 1strbasOLD 17264 restid 17478 cayley 19432 gsumval3 19925 gsumzaddlem 19939 kgencn3 23566 hmeores 23779 opnfbas 23850 tsmsf1o 24153 ust0 24228 icchmeo 24971 icchmeoOLD 24972 plyeq0lem 26249 ulmdvlem1 26443 basellem7 27130 basellem9 27132 dchrisumlem3 27535 structvtxvallem 29037 struct2griedg 29045 gsumhashmul 33064 cycpmfvlem 33132 cycpmfv3 33135 constr01 33783 ivthALT 36336 aomclem4 43069 hashnzfzclim 44341 binomcxplemrat 44369 climsuselem1 45622 gsumfsupp 48098 |
| Copyright terms: Public domain | W3C validator |