| 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 4636 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ {𝐴} = {𝐵} |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 {csn 4626 |
| 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-sb 2065 df-clab 2715 df-cleq 2729 df-sn 4627 |
| This theorem is referenced by: fnressn 7178 fressnfv 7180 snriota 7421 xpassen 9106 ids1 14635 s3tpop 14948 bpoly3 16094 strle1 17195 2strop1 17273 ghmeqker 19261 pws1 20322 pwsmgp 20324 lpival 21334 mat1dimelbas 22477 mat1dim0 22479 mat1dimid 22480 mat1dimscm 22481 mat1dimmul 22482 mat1f1o 22484 imasdsf1olem 24383 ehl0 25451 nosupcbv 27747 noinfcbv 27762 bday1s 27876 cutpw2 28417 pw2bday 28418 vtxval3sn 29060 iedgval3sn 29061 uspgr1v1eop 29266 hh0oi 31922 eulerpartlemmf 34377 bnj601 34934 dffv5 35925 zrdivrng 37960 isdrngo1 37963 aks5lem3a 42190 aks5lem7 42201 prjspval2 42623 mapfzcons 42727 mapfzcons1 42728 mapfzcons2 42730 df3o3 43327 fourierdlem80 46201 lmod1zr 48410 setc1oterm 49134 mndtchom 49181 |
| Copyright terms: Public domain | W3C validator |