Theorem s1fv 14758

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 14745	. . 3 ⊢ (𝐴 ∈ 𝐵 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
2	1	fveq1d 6887	. 2 ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = ({⟨0, 𝐴⟩}‘0))
3		0nn0 12621	. . 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 4583  ⟨cop 4589  ‘cfv 6538  0cc0 11200  ℕ₀cn0 12606  ⟨“cs1 14742

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 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-i2m1 11268

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 4584  df-pr 4586  df-op 4590  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 12607  df-s1 14743

This theorem is used by:  lsws1  14759  eqs1  14760  wrdl1s1  14762  ccats1val2  14775  ccat1st1st  14776  ccat2s1p1  14777  ccat2s1p2  14778  cats1un  14870  revs1  14914  cats1fvn  15009  s2fv0  15038  efgsval2  19947  efgs1  19949  efgsp1  19951  efgsfo  19953  pgpfaclem1  20297  loopclwwlkn1b  30633  clwwlkn1loopb  30634  clwwlknon1  30688  0wlkons1  30712  1wlkdlem4  30731  wlk2v2elem2  30757  ccatws1f1o  33556  cycpmco2lem2  33730  fldext2chn  34402  constrextdg2  34423  signstf0  35239  signsvtn0  35241  signstfvneq0  35243