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

Theorem s1fv 14505
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 14493 . . 3 (𝐴𝐵 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
21fveq1d 6849 . 2 (𝐴𝐵 → (⟨“𝐴”⟩‘0) = ({⟨0, 𝐴⟩}‘0))
3 0nn0 12435 . . 3 0 ∈ ℕ0
4 fvsng 7131 . . 3 ((0 ∈ ℕ0𝐴𝐵) → ({⟨0, 𝐴⟩}‘0) = 𝐴)
53, 4mpan 689 . 2 (𝐴𝐵 → ({⟨0, 𝐴⟩}‘0) = 𝐴)
62, 5eqtrd 2777 1 (𝐴𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  {csn 4591  cop 4597  cfv 6501  0cc0 11058  0cn0 12420  ⟨“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-10 2138  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-mulcl 11120  ax-i2m1 11126
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-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  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-opab 5173  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6453  df-fun 6503  df-fv 6509  df-n0 12421  df-s1 14491
This theorem is referenced by:  lsws1  14506  eqs1  14507  wrdl1s1  14509  ccats1val2  14522  ccat1st1st  14523  ccat2s1p1  14524  ccat2s1p2  14525  cats1un  14616  revs1  14660  cats1fvn  14754  s2fv0  14783  efgsval2  19522  efgs1  19524  efgsp1  19526  efgsfo  19528  pgpfaclem1  19867  loopclwwlkn1b  29028  clwwlkn1loopb  29029  clwwlknon1  29083  0wlkons1  29107  1wlkdlem4  29126  wlk2v2elem2  29142  cycpmco2lem2  32018  signstf0  33220  signsvtn0  33222  signstfvneq0  33224  singoutnword  45195
  Copyright terms: Public domain W3C validator