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 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 ) ) )