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	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( ⟨“ 𝑆 ”⟩ = ⟨“ 𝑇 ”⟩ ↔ 𝑆 = 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		s1val	⊢ ( 𝑆 ∈ 𝐴 → ⟨“ 𝑆 ”⟩ = { ⟨ 0 , 𝑆 ⟩ } )
2		s1val	⊢ ( 𝑇 ∈ 𝐴 → ⟨“ 𝑇 ”⟩ = { ⟨ 0 , 𝑇 ⟩ } )
3	1 2	eqeqan12d	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( ⟨“ 𝑆 ”⟩ = ⟨“ 𝑇 ”⟩ ↔ { ⟨ 0 , 𝑆 ⟩ } = { ⟨ 0 , 𝑇 ⟩ } ) )
4		opex	⊢ ⟨ 0 , 𝑆 ⟩ ∈ V
5		sneqbg	⊢ ( ⟨ 0 , 𝑆 ⟩ ∈ V → ( { ⟨ 0 , 𝑆 ⟩ } = { ⟨ 0 , 𝑇 ⟩ } ↔ ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ) )
6	4 5	mp1i	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( { ⟨ 0 , 𝑆 ⟩ } = { ⟨ 0 , 𝑇 ⟩ } ↔ ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ) )
7		0z	⊢ 0 ∈ ℤ
8		eqid	⊢ 0 = 0
9		opthg	⊢ ( ( 0 ∈ ℤ ∧ 𝑆 ∈ 𝐴 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ ( 0 = 0 ∧ 𝑆 = 𝑇 ) ) )
10	9	baibd	⊢ ( ( ( 0 ∈ ℤ ∧ 𝑆 ∈ 𝐴 ) ∧ 0 = 0 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) )
11	8 10	mpan2	⊢ ( ( 0 ∈ ℤ ∧ 𝑆 ∈ 𝐴 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) )
12	7 11	mpan	⊢ ( 𝑆 ∈ 𝐴 → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) )
13	12	adantr	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) )
14	3 6 13	3bitrd	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( ⟨“ 𝑆 ”⟩ = ⟨“ 𝑇 ”⟩ ↔ 𝑆 = 𝑇 ) )