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 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ AB ”⟩ = ⟨“ CD ”⟩ ↔ A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 s2eq2s1eq ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ AB ”⟩ = ⟨“ CD ”⟩ ↔ ⟨“ A ”⟩ = ⟨“ C ”⟩ ∧ ⟨“ B ”⟩ = ⟨“ D ”⟩
2 s111 ⊢ A ∈ V ∧ C ∈ V → ⟨“ A ”⟩ = ⟨“ C ”⟩ ↔ A = C
3 2 ad2ant2r ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ A ”⟩ = ⟨“ C ”⟩ ↔ A = C
4 s111 ⊢ B ∈ V ∧ D ∈ V → ⟨“ B ”⟩ = ⟨“ D ”⟩ ↔ B = D
5 4 ad2ant2l ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ B ”⟩ = ⟨“ D ”⟩ ↔ B = D
6 3 5 anbi12d ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ A ”⟩ = ⟨“ C ”⟩ ∧ ⟨“ B ”⟩ = ⟨“ D ”⟩ ↔ A = C ∧ B = D
7 1 6 bitrd ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ⟨“ AB ”⟩ = ⟨“ CD ”⟩ ↔ A = C ∧ B = D