# Metamath Proof Explorer

## Theorem xp1st

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

Ref Expression
Assertion xp1st ${⊢}{A}\in \left({B}×{C}\right)\to {1}^{st}\left({A}\right)\in {B}$

### 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 op1std ${⊢}{A}=⟨{b},{c}⟩\to {1}^{st}\left({A}\right)={b}$
5 4 eleq1d ${⊢}{A}=⟨{b},{c}⟩\to \left({1}^{st}\left({A}\right)\in {B}↔{b}\in {B}\right)$
6 5 biimpar ${⊢}\left({A}=⟨{b},{c}⟩\wedge {b}\in {B}\right)\to {1}^{st}\left({A}\right)\in {B}$
7 6 adantrr ${⊢}\left({A}=⟨{b},{c}⟩\wedge \left({b}\in {B}\wedge {c}\in {C}\right)\right)\to {1}^{st}\left({A}\right)\in {B}$
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 {1}^{st}\left({A}\right)\in {B}$
9 1 8 sylbi ${⊢}{A}\in \left({B}×{C}\right)\to {1}^{st}\left({A}\right)\in {B}$