Theorem s1fv 14762

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

Step	Hyp	Ref	Expression
1		s1val 14748	. . 3 ⊢ (𝐴 ∈ 𝐵 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
2	1	fveq1d 6887	. 2 ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = ({⟨0, 𝐴⟩}‘0))
3		0nn0 12624	. . 3 ⊢ 0 ∈ ℕ0
4		fvsng 7185	. . 3 ⊢ ((0 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵) → ({⟨0, 𝐴⟩}‘0) = 𝐴)
5	3, 4	mpan 703	. 2 ⊢ (𝐴 ∈ 𝐵 → ({⟨0, 𝐴⟩}‘0) = 𝐴)
6	2, 5	eqtrd 2795	1 ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {csn 4584  ⟨cop 4834  ‘cfv 6538  0cc0 11203  ℕ₀cn0 12609  ⟨“cs1 14745

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-mulcl 11265  ax-i2m1 11271

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fv 6546  df-n0 12610  df-s1 14746

This theorem is used by:  lsws1  14763  eqs1  14764  wrdl1s1  14766  ccats1val2  14779  ccat1st1st  14780  ccat2s1p1  14781  ccat2s1p2  14782  cats1un  14874  revs1  14918  cats1fvn  15013  s2fv0  15042  efgsval2  19952  efgs1  19954  efgsp1  19956  efgsfo  19958  pgpfaclem1  20302  loopclwwlkn1b  30638  clwwlkn1loopb  30639  clwwlknon1  30693  0wlkons1  30717  1wlkdlem4  30736  wlk2v2elem2  30762  ccatws1f1o  33560  cycpmco2lem2  33734  fldext2chn  34406  constrextdg2  34427  signstf0  35243  signsvtn0  35245  signstfvneq0  35247