Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > s1eqd | Structured version Visualization version GIF version |
Description: Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
Ref | Expression |
---|---|
s1eqd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
s1eqd | ⊢ (𝜑 → 〈“𝐴”〉 = 〈“𝐵”〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s1eqd.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | s1eq 13945 | . 2 ⊢ (𝐴 = 𝐵 → 〈“𝐴”〉 = 〈“𝐵”〉) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 〈“𝐴”〉 = 〈“𝐵”〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 〈“cs1 13940 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-iota 6283 df-fv 6332 df-s1 13941 |
This theorem is referenced by: s1prc 13949 ccat1st1st 13975 swrds1 14019 swrdlsw 14020 reuccatpfxs1lem 14099 s2eqd 14216 s3eqd 14217 s4eqd 14218 s5eqd 14219 s6eqd 14220 s7eqd 14221 s8eqd 14222 frmdgsum 18019 psgnunilem5 18614 efgredlemc 18863 vrgpval 18885 vrgpinv 18887 frgpup2 18894 frgpup3lem 18895 pfx1s2 30641 pfxlsw2ccat 30652 iwrdsplit 31755 sseqval 31756 sseqf 31760 sseqp1 31763 signsvtn0 31950 signstfveq0 31957 mrsubcv 32870 |
Copyright terms: Public domain | W3C validator |