brsnop

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

		Ref	Expression
	Assertion	brsnop	$⊢ (A \in V \land B \in W) \to (X \{⟨A, B⟩\} Y \leftrightarrow (X = A \land Y = B))$

Step	Hyp	Ref	Expression
1		df-br	$⊢ X \{⟨A, B⟩\} Y \leftrightarrow ⟨X, Y⟩ \in \{⟨A, B⟩\}$
2		opex	$⊢ ⟨X, Y⟩ \in V$
3	2	elsn	$⊢ ⟨X, Y⟩ \in \{⟨A, B⟩\} \leftrightarrow ⟨X, Y⟩ = ⟨A, B⟩$
4		opthg2	$⊢ (A \in V \land B \in W) \to (⟨X, Y⟩ = ⟨A, B⟩ \leftrightarrow (X = A \land Y = B))$
5	3 4	bitrid	$⊢ (A \in V \land B \in W) \to (⟨X, Y⟩ \in \{⟨A, B⟩\} \leftrightarrow (X = A \land Y = B))$
6	1 5	bitrid	$⊢ (A \in V \land B \in W) \to (X \{⟨A, B⟩\} Y \leftrightarrow (X = A \land Y = B))$

Metamath Proof Explorer