| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > s1eq | Structured version Visualization version GIF version | ||
| Description: Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| Ref | Expression |
|---|---|
| s1eq | ⊢ (𝐴 = 𝐵 → 〈“𝐴”〉 = 〈“𝐵”〉) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fveq2 6871 | . . . 4 ⊢ (𝐴 = 𝐵 → ( I ‘𝐴) = ( I ‘𝐵)) | |
| 2 | 1 | opeq2d 4841 | . . 3 ⊢ (𝐴 = 𝐵 → 〈0, ( I ‘𝐴)〉 = 〈0, ( I ‘𝐵)〉) |
| 3 | 2 | sneqd 4597 | . 2 ⊢ (𝐴 = 𝐵 → {〈0, ( I ‘𝐴)〉} = {〈0, ( I ‘𝐵)〉}) |
| 4 | df-s1 14624 | . 2 ⊢ 〈“𝐴”〉 = {〈0, ( I ‘𝐴)〉} | |
| 5 | df-s1 14624 | . 2 ⊢ 〈“𝐵”〉 = {〈0, ( I ‘𝐵)〉} | |
| 6 | 3, 4, 5 | 3eqtr4g 2825 | 1 ⊢ (𝐴 = 𝐵 → 〈“𝐴”〉 = 〈“𝐵”〉) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1563 {csn 4585 〈cop 4591 I cid 5546 ‘cfv 6525 0cc0 11088 〈“cs1 14623 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-br 5106 df-iota 6481 df-fv 6533 df-s1 14624 |
| This theorem is referenced by: s1eqd 14629 wrdl1exs1 14641 wrdl1s1 14642 ccats1pfxeqrex 14742 wrdind 14749 wrd2ind 14750 reuccatpfxs1lem 14773 reuccatpfxs1 14774 revs1 14792 chninf 18681 vrmdval 18906 frgpup3lem 19838 vdegp1ci 29797 clwwlknonwwlknonb 30366 mrsubcv 35873 mrsubrn 35876 elmrsubrn 35883 mrsubvrs 35885 mvhval 35897 |
| Copyright terms: Public domain | W3C validator |