s1fv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > s1fv		Structured version Visualization version GIF version

Theorem s1fv 14582

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 14570	. . 3 ⊢ (𝐴 ∈ 𝐵 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
2	1	fveq1d 6863	. 2 ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = ({⟨0, 𝐴⟩}‘0))
3		0nn0 12464	. . 3 ⊢ 0 ∈ ℕ₀
4		fvsng 7157	. . 3 ⊢ ((0 ∈ ℕ₀ ∧ 𝐴 ∈ 𝐵) → ({⟨0, 𝐴⟩}‘0) = 𝐴)
5	3, 4	mpan 690	. 2 ⊢ (𝐴 ∈ 𝐵 → ({⟨0, 𝐴⟩}‘0) = 𝐴)
6	2, 5	eqtrd 2765	1 ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2109 {csn 4592 ⟨cop 4598 ‘cfv 6514 0cc0 11075 ℕ₀cn0 12449 ⟨“cs1 14567

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 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pr 5390 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-mulcl 11137 ax-i2m1 11143

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-ral 3046 df-rex 3055 df-rab 3409 df-v 3452 df-dif 3920 df-un 3922 df-ss 3934 df-nul 4300 df-if 4492 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-br 5111 df-opab 5173 df-id 5536 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-iota 6467 df-fun 6516 df-fv 6522 df-n0 12450 df-s1 14568

This theorem is referenced by: lsws1 14583 eqs1 14584 wrdl1s1 14586 ccats1val2 14599 ccat1st1st 14600 ccat2s1p1 14601 ccat2s1p2 14602 cats1un 14693 revs1 14737 cats1fvn 14831 s2fv0 14860 efgsval2 19670 efgs1 19672 efgsp1 19674 efgsfo 19676 pgpfaclem1 20020 loopclwwlkn1b 29978 clwwlkn1loopb 29979 clwwlknon1 30033 0wlkons1 30057 1wlkdlem4 30076 wlk2v2elem2 30092 ccatws1f1o 32880 cycpmco2lem2 33091 fldext2chn 33725 constrextdg2 33746 signstf0 34566 signsvtn0 34568 signstfvneq0 34570 singoutnword 46887