![]() |
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 4409 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ {𝐴} = {𝐵} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1656 {csn 4399 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-sn 4400 |
This theorem is referenced by: fnressn 6681 fressnfv 6683 snriota 6901 xpassen 8329 ids1 13664 s3tpop 14037 bpoly3 15168 strle1 16339 2strop1 16354 ghmeqker 18045 pws1 18977 pwsmgp 18979 lpival 19613 mat1dimelbas 20652 mat1dim0 20654 mat1dimid 20655 mat1dimscm 20656 mat1dimmul 20657 mat1f1o 20659 imasdsf1olem 22555 ehl0 23592 vtxval3sn 26348 iedgval3sn 26349 uspgr1v1eop 26553 hh0oi 29313 eulerpartlemmf 30978 bnj601 31532 dffv5 32565 zrdivrng 34293 isdrngo1 34296 mapfzcons 38122 mapfzcons1 38123 mapfzcons2 38125 df3o3 39162 fourierdlem80 41195 lmod1zr 43147 |
Copyright terms: Public domain | W3C validator |