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

Metamath Proof Explorer

Theorem ex-2nd

Description: Example for df-2nd . Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015)

		Ref	Expression
	Assertion	ex-2nd	$⊢ 2^{nd} (⟨3, 4⟩) = 4$

Step	Hyp	Ref	Expression
1		3ex	$⊢ 3 \in V$
2		4re	$⊢ 4 \in ℝ$
3	2	elexi	$⊢ 4 \in V$
4	1 3	op2nd	$⊢ 2^{nd} (⟨3, 4⟩) = 4$