Theorem xp2nd

Description: Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	xp2nd	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ( 2nd ‘ 𝐴 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		elxp	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑏 ∃ 𝑐 ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) )
2		vex	⊢ 𝑏 ∈ V
3		vex	⊢ 𝑐 ∈ V
4	2 3	op2ndd	⊢ ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ → ( 2nd ‘ 𝐴 ) = 𝑐 )
5	4	eleq1d	⊢ ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ → ( ( 2nd ‘ 𝐴 ) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶 ) )
6	5	biimpar	⊢ ( ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑐 ∈ 𝐶 ) → ( 2nd ‘ 𝐴 ) ∈ 𝐶 )
7	6	adantrl	⊢ ( ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 2nd ‘ 𝐴 ) ∈ 𝐶 )
8	7	exlimivv	⊢ ( ∃ 𝑏 ∃ 𝑐 ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 2nd ‘ 𝐴 ) ∈ 𝐶 )
9	1 8	sylbi	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ( 2nd ‘ 𝐴 ) ∈ 𝐶 )