This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opth1g

Description: Equality of the first members of equal ordered pairs. Closed form of opth1 . (Contributed by AV, 14-Oct-2018)

		Ref	Expression
	Assertion	opth1g	$⊢ (A \in V \land B \in W) \to (⟨A, B⟩ = ⟨C, D⟩ \to A = C)$

Step	Hyp	Ref	Expression
1		opthg	$⊢ (A \in V \land B \in W) \to (⟨A, B⟩ = ⟨C, D⟩ \leftrightarrow (A = C \land B = D))$
2		simpl	$⊢ (A = C \land B = D) \to A = C$
3	1 2	biimtrdi	$⊢ (A \in V \land B \in W) \to (⟨A, B⟩ = ⟨C, D⟩ \to A = C)$