Metamath Proof Explorer


Theorem brsnop

Description: Binary relation for an ordered pair singleton. (Contributed by Thierry Arnoux, 23-Sep-2023)

Ref Expression
Assertion brsnop ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌 ↔ ( 𝑋 = 𝐴𝑌 = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 df-br ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } )
2 opex 𝑋 , 𝑌 ⟩ ∈ V
3 2 elsn ( ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
4 opthg2 ( ( 𝐴𝑉𝐵𝑊 ) → ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑋 = 𝐴𝑌 = 𝐵 ) ) )
5 3 4 syl5bb ( ( 𝐴𝑉𝐵𝑊 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ( 𝑋 = 𝐴𝑌 = 𝐵 ) ) )
6 1 5 syl5bb ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌 ↔ ( 𝑋 = 𝐴𝑌 = 𝐵 ) ) )