Theorem s1fv 14534

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 14522	. . 3 ⊢ (𝐴 ∈ 𝐵 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
2	1	fveq1d 6836	. 2 ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = ({⟨0, 𝐴⟩}‘0))
3		0nn0 12416	. . 3 ⊢ 0 ∈ ℕ0
4		fvsng 7126	. . 3 ⊢ ((0 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵) → ({⟨0, 𝐴⟩}‘0) = 𝐴)
5	3, 4	mpan 690	. 2 ⊢ (𝐴 ∈ 𝐵 → ({⟨0, 𝐴⟩}‘0) = 𝐴)
6	2, 5	eqtrd 2771	1 ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {csn 4580  ⟨cop 4586  ‘cfv 6492  0cc0 11026  ℕ₀cn0 12401  ⟨“cs1 14519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-i2m1 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-n0 12402  df-s1 14520

This theorem is referenced by:  lsws1  14535  eqs1  14536  wrdl1s1  14538  ccats1val2  14551  ccat1st1st  14552  ccat2s1p1  14553  ccat2s1p2  14554  cats1un  14644  revs1  14688  cats1fvn  14781  s2fv0  14810  efgsval2  19662  efgs1  19664  efgsp1  19666  efgsfo  19668  pgpfaclem1  20012  loopclwwlkn1b  30117  clwwlkn1loopb  30118  clwwlknon1  30172  0wlkons1  30196  1wlkdlem4  30215  wlk2v2elem2  30231  ccatws1f1o  33033  cycpmco2lem2  33209  fldext2chn  33885  constrextdg2  33906  signstf0  34725  signsvtn0  34727  signstfvneq0  34729