Theorem s111

Description: The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015) (Revised by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	s111	$$⊢\left(S\in A\wedge T\in A\right)\to \left(⟨“S”⟩=⟨“T”⟩\leftrightarrow S=T\right)$$

Proof

Step	Hyp	Ref	Expression
1		s1val	$$⊢S\in A\to ⟨“S”⟩=\left\{⟨0,S⟩\right\}$$
2		s1val	$$⊢T\in A\to ⟨“T”⟩=\left\{⟨0,T⟩\right\}$$
3	1 2	eqeqan12d	$$⊢\left(S\in A\wedge T\in A\right)\to \left(⟨“S”⟩=⟨“T”⟩\leftrightarrow \left\{⟨0,S⟩\right\}=\left\{⟨0,T⟩\right\}\right)$$
4		opex	$$⊢⟨0,S⟩\in \mathrm{V}$$
5		sneqbg	$$⊢⟨0,S⟩\in \mathrm{V}\to \left(\left\{⟨0,S⟩\right\}=\left\{⟨0,T⟩\right\}\leftrightarrow ⟨0,S⟩=⟨0,T⟩\right)$$
6	4 5	mp1i	$$⊢\left(S\in A\wedge T\in A\right)\to \left(\left\{⟨0,S⟩\right\}=\left\{⟨0,T⟩\right\}\leftrightarrow ⟨0,S⟩=⟨0,T⟩\right)$$
7		0z	$$⊢0\in \mathbb{Z}$$
8		eqid	$$⊢0=0$$
9		opthg	$$⊢\left(0\in \mathbb{Z}\wedge S\in A\right)\to \left(⟨0,S⟩=⟨0,T⟩\leftrightarrow \left(0=0\wedge S=T\right)\right)$$
10	9	baibd	$$⊢\left(\left(0\in \mathbb{Z}\wedge S\in A\right)\wedge 0=0\right)\to \left(⟨0,S⟩=⟨0,T⟩\leftrightarrow S=T\right)$$
11	8 10	mpan2	$$⊢\left(0\in \mathbb{Z}\wedge S\in A\right)\to \left(⟨0,S⟩=⟨0,T⟩\leftrightarrow S=T\right)$$
12	7 11	mpan	$$⊢S\in A\to \left(⟨0,S⟩=⟨0,T⟩\leftrightarrow S=T\right)$$
13	12	adantr	$$⊢\left(S\in A\wedge T\in A\right)\to \left(⟨0,S⟩=⟨0,T⟩\leftrightarrow S=T\right)$$
14	3 6 13	3bitrd	$$⊢\left(S\in A\wedge T\in A\right)\to \left(⟨“S”⟩=⟨“T”⟩\leftrightarrow S=T\right)$$