Description: Equality conditions for ordered pairs <. A , A >. and <. B , B >. . (Contributed by Peter Mazsa, 22-Jul-2019) (Revised by Thierry Arnoux, 16-Feb-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | opideq | |- ( A e. V -> ( <. A , A >. = <. B , B >. <-> A = B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opthg | |- ( ( A e. V /\ A e. V ) -> ( <. A , A >. = <. B , B >. <-> ( A = B /\ A = B ) ) ) |
|
2 | 1 | anidms | |- ( A e. V -> ( <. A , A >. = <. B , B >. <-> ( A = B /\ A = B ) ) ) |
3 | anidm | |- ( ( A = B /\ A = B ) <-> A = B ) |
|
4 | 2 3 | syl6bb | |- ( A e. V -> ( <. A , A >. = <. B , B >. <-> A = B ) ) |