# Metamath Proof Explorer

## Theorem xp2nd

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

Ref Expression
Assertion xp2nd ${⊢}{A}\in \left({B}×{C}\right)\to {2}^{nd}\left({A}\right)\in {C}$

### Proof

Step Hyp Ref Expression
1 elxp ${⊢}{A}\in \left({B}×{C}\right)↔\exists {b}\phantom{\rule{.4em}{0ex}}\exists {c}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{b},{c}⟩\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)$
2 vex ${⊢}{b}\in \mathrm{V}$
3 vex ${⊢}{c}\in \mathrm{V}$
4 2 3 op2ndd ${⊢}{A}=⟨{b},{c}⟩\to {2}^{nd}\left({A}\right)={c}$
5 4 eleq1d ${⊢}{A}=⟨{b},{c}⟩\to \left({2}^{nd}\left({A}\right)\in {C}↔{c}\in {C}\right)$
6 5 biimpar ${⊢}\left({A}=⟨{b},{c}⟩\wedge {c}\in {C}\right)\to {2}^{nd}\left({A}\right)\in {C}$
7 6 adantrl ${⊢}\left({A}=⟨{b},{c}⟩\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {2}^{nd}\left({A}\right)\in {C}$
8 7 exlimivv ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}\exists {c}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{b},{c}⟩\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {2}^{nd}\left({A}\right)\in {C}$
9 1 8 sylbi ${⊢}{A}\in \left({B}×{C}\right)\to {2}^{nd}\left({A}\right)\in {C}$