This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-s1

Description: Define the canonical injection from symbols to words. Although not required, A should usually be a set. Otherwise, the singleton word <" A "> would be the singleton word consisting of the empty set, see s1prc , and not, as maybe expected, the empty word, see also s1nz . (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

		Ref	Expression
	Assertion	df-s1	⊢ ⟨“ 𝐴 ”⟩ = { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	cs1	⊢ ⟨“ 𝐴 ”⟩
2		cc0	⊢ 0
3		cid	⊢ I
4	0 3	cfv	⊢ ( I ‘ 𝐴 )
5	2 4	cop	⊢ ⟨ 0 , ( I ‘ 𝐴 ) ⟩
6	5	csn	⊢ { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ }
7	1 6	wceq	⊢ ⟨“ 𝐴 ”⟩ = { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ }