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

Theorem s1eqd 14496
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 14495 . 2 (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
31, 2syl 17 1 (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  ⟨“cs1 14490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-s1 14491
This theorem is referenced by:  s1prc  14499  ccat1st1st  14523  swrds1  14561  swrdlsw  14562  reuccatpfxs1lem  14641  s2eqd  14759  s3eqd  14760  s4eqd  14761  s5eqd  14762  s6eqd  14763  s7eqd  14764  s8eqd  14765  frmdgsum  18679  psgnunilem5  19283  efgredlemc  19534  vrgpval  19556  vrgpinv  19558  frgpup2  19565  frgpup3lem  19566  pfx1s2  31837  pfxlsw2ccat  31848  iwrdsplit  33027  sseqval  33028  sseqf  33032  sseqp1  33035  signsvtn0  33222  signstfveq0  33229  mrsubcv  34144
  Copyright terms: Public domain W3C validator