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 | bitrid | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ) ) |
6 | 1 5 | bitrid | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌 ↔ ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ) ) |