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	$$⊢\left(A\in V\wedge B\in W\right)\to \left(⟨A,B⟩=⟨C,D⟩\to A=C\right)$$

Proof

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