Theorem op2ndg

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

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

Proof

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