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 e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. -> A = C ) )

Proof

Step Hyp Ref Expression
1 opthg 
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) )
2 simpl 
 |-  ( ( A = C /\ B = D ) -> A = C )
3 1 2 biimtrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. -> A = C ) )