Theorem s1fv 14786

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 14772	. . 3 ⊢ (𝐴 ∈ 𝐵 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
2	1	fveq1d 6910	. 2 ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = ({⟨0, 𝐴⟩}‘0))
3		0nn0 12648	. . 3 ⊢ 0 ∈ ℕ0
4		fvsng 7208	. . 3 ⊢ ((0 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵) → ({⟨0, 𝐴⟩}‘0) = 𝐴)
5	3, 4	mpan 703	. 2 ⊢ (𝐴 ∈ 𝐵 → ({⟨0, 𝐴⟩}‘0) = 𝐴)
6	2, 5	eqtrd 2798	1 ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  {csn 4588  ⟨cop 4838  ‘cfv 6558  0cc0 11227  ℕ₀cn0 12633  ⟨“cs1 14769

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-mulcl 11289  ax-i2m1 11295

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6512  df-fun 6560  df-fv 6566  df-n0 12634  df-s1 14770

This theorem is used by:  lsws1  14787  eqs1  14788  wrdl1s1  14790  ccats1val2  14803  ccat1st1st  14804  ccat2s1p1  14805  ccat2s1p2  14806  cats1un  14898  revs1  14942  cats1fvn  15037  s2fv0  15066  efgsval2  19977  efgs1  19979  efgsp1  19981  efgsfo  19983  pgpfaclem1  20327  loopclwwlkn1b  30663  clwwlkn1loopb  30664  clwwlknon1  30718  0wlkons1  30742  1wlkdlem4  30761  wlk2v2elem2  30787  ccatws1f1o  33584  cycpmco2lem2  33758  fldext2chn  34430  constrextdg2  34451  signstf0  35267  signsvtn0  35269  signstfvneq0  35271