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 e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" A B "> = <" C D "> <-> ( A = C /\ B = D ) ) )

Proof

Step	Hyp	Ref	Expression
1		s2eq2s1eq	|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" A B "> = <" C D "> <-> ( <" A "> = <" C "> /\ <" B "> = <" D "> ) ) )
2		s111	|- ( ( A e. V /\ C e. V ) -> ( <" A "> = <" C "> <-> A = C ) )
3	2	ad2ant2r	|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" A "> = <" C "> <-> A = C ) )
4		s111	|- ( ( B e. V /\ D e. V ) -> ( <" B "> = <" D "> <-> B = D ) )
5	4	ad2ant2l	|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" B "> = <" D "> <-> B = D ) )
6	3 5	anbi12d	|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( <" A "> = <" C "> /\ <" B "> = <" D "> ) <-> ( A = C /\ B = D ) ) )
7	1 6	bitrd	|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" A B "> = <" C D "> <-> ( A = C /\ B = D ) ) )