xp1st

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

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

Step	Hyp	Ref	Expression
1		elxp	$⊢ A \in (B \times C) \leftrightarrow \exists b \exists c (A = ⟨b, c⟩ \land (b \in B \land c \in C))$
2		vex	$⊢ b \in V$
3		vex	$⊢ c \in V$
4	2 3	op1std	$⊢ A = ⟨b, c⟩ \to 1^{st} (A) = b$
5	4	eleq1d	$⊢ A = ⟨b, c⟩ \to (1^{st} (A) \in B \leftrightarrow b \in B)$
6	5	biimpar	$⊢ (A = ⟨b, c⟩ \land b \in B) \to 1^{st} (A) \in B$
7	6	adantrr	$⊢ (A = ⟨b, c⟩ \land (b \in B \land c \in C)) \to 1^{st} (A) \in B$
8	7	exlimivv	$⊢ \exists b \exists c (A = ⟨b, c⟩ \land (b \in B \land c \in C)) \to 1^{st} (A) \in B$
9	1 8	sylbi	$⊢ A \in (B \times C) \to 1^{st} (A) \in B$

Metamath Proof Explorer