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	$⊢ (S \in A \land T \in A) \to (⟨“ S ”⟩ = ⟨“ T ”⟩ \leftrightarrow S = T)$

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

Metamath Proof Explorer