![]() |
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 6499 | . . . 4 ⊢ (𝐴 = 𝐵 → ( I ‘𝐴) = ( I ‘𝐵)) | |
2 | 1 | opeq2d 4684 | . . 3 ⊢ (𝐴 = 𝐵 → 〈0, ( I ‘𝐴)〉 = 〈0, ( I ‘𝐵)〉) |
3 | 2 | sneqd 4453 | . 2 ⊢ (𝐴 = 𝐵 → {〈0, ( I ‘𝐴)〉} = {〈0, ( I ‘𝐵)〉}) |
4 | df-s1 13759 | . 2 ⊢ 〈“𝐴”〉 = {〈0, ( I ‘𝐴)〉} | |
5 | df-s1 13759 | . 2 ⊢ 〈“𝐵”〉 = {〈0, ( I ‘𝐵)〉} | |
6 | 3, 4, 5 | 3eqtr4g 2839 | 1 ⊢ (𝐴 = 𝐵 → 〈“𝐴”〉 = 〈“𝐵”〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 {csn 4441 〈cop 4447 I cid 5311 ‘cfv 6188 0cc0 10335 〈“cs1 13758 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-rex 3094 df-rab 3097 df-v 3417 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-iota 6152 df-fv 6196 df-s1 13759 |
This theorem is referenced by: s1eqd 13764 wrdl1exs1 13776 wrdl1s1 13777 ccats1pfxeqrex 13906 wrdind 13915 wrdindOLD 13916 wrd2ind 13917 wrd2indOLD 13918 ccats1swrdeqrexOLD 13919 reuccats1lemOLD 13920 reuccats1OLD 13921 reuccatpfxs1lem 13955 reuccatpfxs1 13956 revs1 13984 vrmdval 17863 frgpup3lem 18663 vdegp1ci 27023 clwwlknonwwlknonb 27634 mrsubcv 32283 mrsubrn 32286 elmrsubrn 32293 mrsubvrs 32295 mvhval 32307 |
Copyright terms: Public domain | W3C validator |