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\times C\right)\to 1^{st}\left(A\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		elxp	$$⊢A\in \left(B\times C\right)\leftrightarrow \exists b\exists c\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\leftrightarrow 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\exists c\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\times C\right)\to 1^{st}\left(A\right)\in B$$