op2ndg

Description: Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005)

		Ref	Expression
	Assertion	op2ndg	$⊢ (A \in V \land B \in W) \to 2^{nd} (⟨A, B⟩) = B$

Step	Hyp	Ref	Expression
1		opeq1	$⊢ x = A \to ⟨x, y⟩ = ⟨A, y⟩$
2	1	fveqeq2d	$⊢ x = A \to (2^{nd} (⟨x, y⟩) = y \leftrightarrow 2^{nd} (⟨A, y⟩) = y)$
3		opeq2	$⊢ y = B \to ⟨A, y⟩ = ⟨A, B⟩$
4	3	fveq2d	$⊢ y = B \to 2^{nd} (⟨A, y⟩) = 2^{nd} (⟨A, B⟩)$
5		id	$⊢ y = B \to y = B$
6	4 5	eqeq12d	$⊢ y = B \to (2^{nd} (⟨A, y⟩) = y \leftrightarrow 2^{nd} (⟨A, B⟩) = B)$
7		vex	$⊢ x \in V$
8		vex	$⊢ y \in V$
9	7 8	op2nd	$⊢ 2^{nd} (⟨x, y⟩) = y$
10	2 6 9	vtocl2g	$⊢ (A \in V \land B \in W) \to 2^{nd} (⟨A, B⟩) = B$

Metamath Proof Explorer