Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sneqi | Structured version Visualization version GIF version |
Description: Equality inference for singletons. (Contributed by NM, 22-Jan-2004.) |
Ref | Expression |
---|---|
sneqi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
sneqi | ⊢ {𝐴} = {𝐵} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sneqi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | sneq 4567 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ {𝐴} = {𝐵} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 {csn 4557 |
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-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-sn 4558 |
This theorem is referenced by: fnressn 6912 fressnfv 6914 snriota 7136 xpassen 8599 ids1 13939 s3tpop 14259 bpoly3 15400 strle1 16580 2strop1 16595 ghmeqker 18323 pws1 19295 pwsmgp 19297 lpival 19946 mat1dimelbas 21008 mat1dim0 21010 mat1dimid 21011 mat1dimscm 21012 mat1dimmul 21013 mat1f1o 21015 imasdsf1olem 22910 ehl0 23947 vtxval3sn 26755 iedgval3sn 26756 uspgr1v1eop 26958 hh0oi 29607 eulerpartlemmf 31532 bnj601 32091 dffv5 33282 zrdivrng 35112 isdrngo1 35115 fnimasnd 38999 prjspval2 39141 mapfzcons 39191 mapfzcons1 39192 mapfzcons2 39194 df3o3 40253 fourierdlem80 42348 lmod1zr 44476 |
Copyright terms: Public domain | W3C validator |