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 | ⊢ ( 𝐴 ∈ 𝑉 → ( 〈 𝐴 , 𝐴 〉 = 〈 𝐵 , 𝐵 〉 ↔ 𝐴 = 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opthg | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 〈 𝐴 , 𝐴 〉 = 〈 𝐵 , 𝐵 〉 ↔ ( 𝐴 = 𝐵 ∧ 𝐴 = 𝐵 ) ) ) | |
2 | 1 | anidms | ⊢ ( 𝐴 ∈ 𝑉 → ( 〈 𝐴 , 𝐴 〉 = 〈 𝐵 , 𝐵 〉 ↔ ( 𝐴 = 𝐵 ∧ 𝐴 = 𝐵 ) ) ) |
3 | anidm | ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐴 = 𝐵 ) ↔ 𝐴 = 𝐵 ) | |
4 | 2 3 | syl6bb | ⊢ ( 𝐴 ∈ 𝑉 → ( 〈 𝐴 , 𝐴 〉 = 〈 𝐵 , 𝐵 〉 ↔ 𝐴 = 𝐵 ) ) |