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