Metamath Proof Explorer

Theorem s2eq2seq

Description: Two length 2 words are equal iff the corresponding symbols are equal. (Contributed by AV, 20-Oct-2018)

Ref Expression
Assertion s2eq2seq ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐶 𝐷 ”⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 s2eq2s1eq ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐶 𝐷 ”⟩ ↔ ( ⟨“ 𝐴 ”⟩ = ⟨“ 𝐶 ”⟩ ∧ ⟨“ 𝐵 ”⟩ = ⟨“ 𝐷 ”⟩ ) ) )
2 s111 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 ”⟩ = ⟨“ 𝐶 ”⟩ ↔ 𝐴 = 𝐶 ) )
3 2 ad2ant2r ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 ”⟩ = ⟨“ 𝐶 ”⟩ ↔ 𝐴 = 𝐶 ) )
4 s111 ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( ⟨“ 𝐵 ”⟩ = ⟨“ 𝐷 ”⟩ ↔ 𝐵 = 𝐷 ) )
5 4 ad2ant2l ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ⟨“ 𝐵 ”⟩ = ⟨“ 𝐷 ”⟩ ↔ 𝐵 = 𝐷 ) )
6 3 5 anbi12d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ⟨“ 𝐴 ”⟩ = ⟨“ 𝐶 ”⟩ ∧ ⟨“ 𝐵 ”⟩ = ⟨“ 𝐷 ”⟩ ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
7 1 6 bitrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐶 𝐷 ”⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )