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

Theorem s1fv 13590
Description: Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
s1fv (𝐴𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)

Proof of Theorem s1fv
StepHypRef Expression
1 s1val 13578 . . 3 (𝐴𝐵 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
21fveq1d 6335 . 2 (𝐴𝐵 → (⟨“𝐴”⟩‘0) = ({⟨0, 𝐴⟩}‘0))
3 0nn0 11514 . . 3 0 ∈ ℕ0
4 fvsng 6594 . . 3 ((0 ∈ ℕ0𝐴𝐵) → ({⟨0, 𝐴⟩}‘0) = 𝐴)
53, 4mpan 670 . 2 (𝐴𝐵 → ({⟨0, 𝐴⟩}‘0) = 𝐴)
62, 5eqtrd 2805 1 (𝐴𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145  {csn 4317  cop 4323  cfv 6030  0cc0 10142  0cn0 11499  ⟨“cs1 13490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035  ax-1cn 10200  ax-icn 10201  ax-addcl 10202  ax-mulcl 10204  ax-i2m1 10210
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-iota 5993  df-fun 6032  df-fv 6038  df-n0 11500  df-s1 13498
This theorem is referenced by:  lsws1  13591  eqs1  13592  wrdl1s1  13594  ccats1val2  13610  ccat1st1st  13611  ccat2s1p1  13612  ccat2s1p2  13613  cats1un  13684  revs1  13723  cats1fvn  13812  s2fv0  13841  efgsval2  18353  efgs1  18355  efgsp1  18357  efgsfo  18359  pgpfaclem1  18688  loopclwwlkn1b  27198  clwwlkn1loopb  27199  clwwlknon1  27272  0wlkons1  27301  1wlkdlem4  27320  wlk2v2elem2  27336  signstf0  30985  signstfvn  30986  signsvtn0  30987  signstfvneq0  30989
  Copyright terms: Public domain W3C validator