![]() |
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 13690 | . 2 ⊢ (𝐴 = 𝐵 → 〈“𝐴”〉 = 〈“𝐵”〉) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 〈“𝐴”〉 = 〈“𝐵”〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 〈“cs1 13685 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-iota 6099 df-fv 6143 df-s1 13686 |
This theorem is referenced by: s1prc 13694 ccat1st1st 13718 swrds1 13771 swrdlsw 13772 swrdccatwrdOLD 13830 reuccatpfxs1lem 13882 s2eqd 14014 s3eqd 14015 s4eqd 14016 s5eqd 14017 s6eqd 14018 s7eqd 14019 s8eqd 14020 frmdgsum 17786 psgnunilem5 18297 psgnunilem5OLD 18298 efgredlemc 18543 vrgpval 18566 vrgpinv 18568 frgpup2 18575 frgpup3lem 18576 iwrdsplit 31047 iwrdsplitOLD 31048 sseqval 31049 sseqf 31053 sseqp1 31056 signsvtn0 31247 signsvtn0OLD 31248 signstfveq0 31255 signstfveq0OLD 31256 mrsubcv 32006 |
Copyright terms: Public domain | W3C validator |