Theorem op2ndg

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

	Ref	Expression
Assertion	op2ndg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		opeq1	⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
2	1	fveqeq2d	⊢ ( 𝑥 = 𝐴 → ( ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦 ↔ ( 2nd ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = 𝑦 ) )
3		opeq2	⊢ ( 𝑦 = 𝐵 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
4	3	fveq2d	⊢ ( 𝑦 = 𝐵 → ( 2nd ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
5		id	⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
6	4 5	eqeq12d	⊢ ( 𝑦 = 𝐵 → ( ( 2nd ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = 𝑦 ↔ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 ) )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	op2nd	⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
10	2 6 9	vtocl2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )