|   | 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 14638 | . 2 ⊢ (𝐴 = 𝐵 → 〈“𝐴”〉 = 〈“𝐵”〉) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 〈“𝐴”〉 = 〈“𝐵”〉) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1540 〈“cs1 14633 | 
| 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-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-s1 14634 | 
| This theorem is referenced by: s1prc 14642 ccat1st1st 14666 swrds1 14704 swrdlsw 14705 reuccatpfxs1lem 14784 s2eqd 14902 s3eqd 14903 s4eqd 14904 s5eqd 14905 s6eqd 14906 s7eqd 14907 s8eqd 14908 frmdgsum 18875 psgnunilem5 19512 efgredlemc 19763 vrgpval 19785 vrgpinv 19787 frgpup2 19794 frgpup3lem 19795 pfx1s2 32923 pfxlsw2ccat 32935 ccatws1f1olast 32937 wrdpmtrlast 33113 1arithidomlem2 33564 iwrdsplit 34389 sseqval 34390 sseqf 34394 sseqp1 34397 signsvtn0 34585 signstfveq0 34592 mrsubcv 35515 | 
| Copyright terms: Public domain | W3C validator |