xp2nd

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

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

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	op2ndd	$⊢ A = ⟨b, c⟩ \to 2^{nd} (A) = c$
5	4	eleq1d	$⊢ A = ⟨b, c⟩ \to (2^{nd} (A) \in C \leftrightarrow c \in C)$
6	5	biimpar	$⊢ (A = ⟨b, c⟩ \land c \in C) \to 2^{nd} (A) \in C$
7	6	adantrl	$⊢ (A = ⟨b, c⟩ \land (b \in B \land c \in C)) \to 2^{nd} (A) \in C$
8	7	exlimivv	$⊢ \exists b \exists c (A = ⟨b, c⟩ \land (b \in B \land c \in C)) \to 2^{nd} (A) \in C$
9	1 8	sylbi	$⊢ A \in (B \times C) \to 2^{nd} (A) \in C$

Metamath Proof Explorer