Description: Binary relation for an ordered pair singleton. (Contributed by Thierry Arnoux, 23-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | brsnop | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑋 { 〈 𝐴 , 𝐵 〉 } 𝑌 ↔ ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-br | ⊢ ( 𝑋 { 〈 𝐴 , 𝐵 〉 } 𝑌 ↔ 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝐴 , 𝐵 〉 } ) | |
2 | opex | ⊢ 〈 𝑋 , 𝑌 〉 ∈ V | |
3 | 2 | elsn | ⊢ ( 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝐴 , 𝐵 〉 } ↔ 〈 𝑋 , 𝑌 〉 = 〈 𝐴 , 𝐵 〉 ) |
4 | opthg2 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 〈 𝑋 , 𝑌 〉 = 〈 𝐴 , 𝐵 〉 ↔ ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ) ) | |
5 | 3 4 | syl5bb | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝐴 , 𝐵 〉 } ↔ ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ) ) |
6 | 1 5 | syl5bb | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑋 { 〈 𝐴 , 𝐵 〉 } 𝑌 ↔ ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ) ) |