Theorem s1fv 14566

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 14554	. . 3 ⊢ (𝐴 ∈ 𝐵 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
2	1	fveq1d 6894	. 2 ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = ({⟨0, 𝐴⟩}‘0))
3		0nn0 12493	. . 3 ⊢ 0 ∈ ℕ0
4		fvsng 7181	. . 3 ⊢ ((0 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵) → ({⟨0, 𝐴⟩}‘0) = 𝐴)
5	3, 4	mpan 686	. 2 ⊢ (𝐴 ∈ 𝐵 → ({⟨0, 𝐴⟩}‘0) = 𝐴)
6	2, 5	eqtrd 2770	1 ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  {csn 4629  ⟨cop 4635  ‘cfv 6544  0cc0 11114  ℕ₀cn0 12478  ⟨“cs1 14551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-mulcl 11176  ax-i2m1 11182

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552  df-n0 12479  df-s1 14552

This theorem is referenced by:  lsws1  14567  eqs1  14568  wrdl1s1  14570  ccats1val2  14583  ccat1st1st  14584  ccat2s1p1  14585  ccat2s1p2  14586  cats1un  14677  revs1  14721  cats1fvn  14815  s2fv0  14844  efgsval2  19644  efgs1  19646  efgsp1  19648  efgsfo  19650  pgpfaclem1  19994  loopclwwlkn1b  29560  clwwlkn1loopb  29561  clwwlknon1  29615  0wlkons1  29639  1wlkdlem4  29658  wlk2v2elem2  29674  cycpmco2lem2  32554  signstf0  33875  signsvtn0  33877  signstfvneq0  33879  singoutnword  45896