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 \in V \land B \in V) \land (C \in V \land D \in V)) \to (⟨“ A B ”⟩ = ⟨“ C D ”⟩ \leftrightarrow (A = C \land B = D))$

Step	Hyp	Ref	Expression
1		s2eq2s1eq	$⊢ ((A \in V \land B \in V) \land (C \in V \land D \in V)) \to (⟨“ A B ”⟩ = ⟨“ C D ”⟩ \leftrightarrow (⟨“ A ”⟩ = ⟨“ C ”⟩ \land ⟨“ B ”⟩ = ⟨“ D ”⟩))$
2		s111	$⊢ (A \in V \land C \in V) \to (⟨“ A ”⟩ = ⟨“ C ”⟩ \leftrightarrow A = C)$
3	2	ad2ant2r	$⊢ ((A \in V \land B \in V) \land (C \in V \land D \in V)) \to (⟨“ A ”⟩ = ⟨“ C ”⟩ \leftrightarrow A = C)$
4		s111	$⊢ (B \in V \land D \in V) \to (⟨“ B ”⟩ = ⟨“ D ”⟩ \leftrightarrow B = D)$
5	4	ad2ant2l	$⊢ ((A \in V \land B \in V) \land (C \in V \land D \in V)) \to (⟨“ B ”⟩ = ⟨“ D ”⟩ \leftrightarrow B = D)$
6	3 5	anbi12d	$⊢ ((A \in V \land B \in V) \land (C \in V \land D \in V)) \to ((⟨“ A ”⟩ = ⟨“ C ”⟩ \land ⟨“ B ”⟩ = ⟨“ D ”⟩) \leftrightarrow (A = C \land B = D))$
7	1 6	bitrd	$⊢ ((A \in V \land B \in V) \land (C \in V \land D \in V)) \to (⟨“ A B ”⟩ = ⟨“ C D ”⟩ \leftrightarrow (A = C \land B = D))$

Metamath Proof Explorer