op1stg

Description: Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005)

		Ref	Expression
	Assertion	op1stg	$⊢ (A \in V \land B \in W) \to 1^{st} (⟨A, B⟩) = A$

Step	Hyp	Ref	Expression
1		opeq1	$⊢ x = A \to ⟨x, y⟩ = ⟨A, y⟩$
2	1	fveq2d	$⊢ x = A \to 1^{st} (⟨x, y⟩) = 1^{st} (⟨A, y⟩)$
3		id	$⊢ x = A \to x = A$
4	2 3	eqeq12d	$⊢ x = A \to (1^{st} (⟨x, y⟩) = x \leftrightarrow 1^{st} (⟨A, y⟩) = A)$
5		opeq2	$⊢ y = B \to ⟨A, y⟩ = ⟨A, B⟩$
6	5	fveqeq2d	$⊢ y = B \to (1^{st} (⟨A, y⟩) = A \leftrightarrow 1^{st} (⟨A, B⟩) = A)$
7		vex	$⊢ x \in V$
8		vex	$⊢ y \in V$
9	7 8	op1st	$⊢ 1^{st} (⟨x, y⟩) = x$
10	4 6 9	vtocl2g	$⊢ (A \in V \land B \in W) \to 1^{st} (⟨A, B⟩) = A$

Metamath Proof Explorer