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 4135 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ {𝐴} = {𝐵} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 {csn 4125 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-sn 4126 |
This theorem is referenced by: fnressn 6330 fressnfv 6332 snriota 6540 xpassen 7939 ids1 13230 s3tpop 13504 bpoly3 14628 strlemor1 15796 strle1 15800 2strop1 15814 ghmeqker 17510 pws1 18439 pwsmgp 18441 lpival 19066 mat1dimelbas 20096 mat1dim0 20098 mat1dimid 20099 mat1dimscm 20100 mat1dimmul 20101 mat1f1o 20103 imasdsf1olem 21988 vtxval3sn 25718 iedgval3sn 25719 vdgr1c 26432 hh0oi 28146 eulerpartlemmf 29764 bnj601 30244 dffv5 31201 zrdivrng 32922 isdrngo1 32925 mapfzcons 36297 mapfzcons1 36298 mapfzcons2 36300 df3o3 37343 fourierdlem80 39079 uspgr1v1eop 40475 lmod1zr 42076 |
Copyright terms: Public domain | W3C validator |