![]() |
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 4640 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ {𝐴} = {𝐵} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 {csn 4630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-sn 4631 |
This theorem is referenced by: fnressn 7167 fressnfv 7169 snriota 7409 xpassen 9091 ids1 14583 s3tpop 14896 bpoly3 16038 strle1 17130 2strop1 17211 ghmeqker 19206 pws1 20273 pwsmgp 20275 lpival 21231 mat1dimelbas 22417 mat1dim0 22419 mat1dimid 22420 mat1dimscm 22421 mat1dimmul 22422 mat1f1o 22424 imasdsf1olem 24323 ehl0 25389 nosupcbv 27681 noinfcbv 27696 bday1s 27810 vtxval3sn 28928 iedgval3sn 28929 uspgr1v1eop 29134 hh0oi 31785 eulerpartlemmf 34126 bnj601 34682 dffv5 35651 zrdivrng 37557 isdrngo1 37560 prjspval2 42172 mapfzcons 42278 mapfzcons1 42279 mapfzcons2 42281 df3o3 42885 fourierdlem80 45712 lmod1zr 47747 mndtchom 48282 |
Copyright terms: Public domain | W3C validator |