MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  s1eqd Structured version   Visualization version   GIF version

Theorem s1eqd 13323
Description: Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
Hypothesis
Ref Expression
s1eqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
s1eqd (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)

Proof of Theorem s1eqd
StepHypRef Expression
1 s1eqd.1 . 2 (𝜑𝐴 = 𝐵)
2 s1eq 13322 . 2 (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
31, 2syl 17 1 (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  ⟨“cs1 13236
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-br 4616  df-iota 5812  df-fv 5857  df-s1 13244
This theorem is referenced by:  swrds1  13392  swrdlsw  13393  swrdccatwrd  13409  s2eqd  13548  s3eqd  13549  s4eqd  13550  s5eqd  13551  s6eqd  13552  s7eqd  13553  s8eqd  13554  frmdgsum  17323  psgnunilem5  17838  efgredlemc  18082  vrgpval  18104  vrgpinv  18106  frgpup2  18113  frgpup3lem  18114  iwrdsplit  30242  sseqval  30243  sseqf  30247  sseqp1  30250  signsvtn0  30439  signstfveq0  30446  mrsubcv  31136  reuccatpfxs1lem  40748  reuccatpfxs1  40749
  Copyright terms: Public domain W3C validator