Theorem s1fv 14571

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  {csn 4562  ⟨cop 4568  ‘cfv 6492  0cc0 11036  ℕ₀cn0 12435  ⟨“cs1 14556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-mulcl 11098  ax-i2m1 11104

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-n0 12436  df-s1 14557

This theorem is referenced by:  lsws1  14572  eqs1  14573  wrdl1s1  14575  ccats1val2  14588  ccat1st1st  14589  ccat2s1p1  14590  ccat2s1p2  14591  cats1un  14681  revs1  14725  cats1fvn  14818  s2fv0  14847  efgsval2  19706  efgs1  19708  efgsp1  19710  efgsfo  19712  pgpfaclem1  20056  loopclwwlkn1b  30137  clwwlkn1loopb  30138  clwwlknon1  30192  0wlkons1  30216  1wlkdlem4  30235  wlk2v2elem2  30251  ccatws1f1o  33037  cycpmco2lem2  33215  fldext2chn  33919  constrextdg2  33940  signstf0  34759  signsvtn0  34761  signstfvneq0  34763