This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovsng

Description: The operation value of a singleton of a nested ordered pair is the last member. (Contributed by Zhi Wang, 22-Oct-2025)

		Ref	Expression
	Assertion	ovsng	$⊢ C \in V \to A \{⟨⟨A, B⟩, C⟩\} B = C$

Step	Hyp	Ref	Expression
1		df-ov	$⊢ A \{⟨⟨A, B⟩, C⟩\} B = \{⟨⟨A, B⟩, C⟩\} (⟨A, B⟩)$
2		opex	$⊢ ⟨A, B⟩ \in V$
3		fvsng	$⊢ (⟨A, B⟩ \in V \land C \in V) \to \{⟨⟨A, B⟩, C⟩\} (⟨A, B⟩) = C$
4	2 3	mpan	$⊢ C \in V \to \{⟨⟨A, B⟩, C⟩\} (⟨A, B⟩) = C$
5	1 4	eqtrid	$⊢ C \in V \to A \{⟨⟨A, B⟩, C⟩\} B = C$