Metamath Proof Explorer

Theorem opth1neg

Description: Two ordered pairs are not equal if their first components are not equal. (Contributed by Zhi Wang, 7-Oct-2025)

		Ref	Expression
	Assertion	opth1neg	\|- ( ( A e. V /\ B e. W ) -> ( A =/= C -> <. A , B >. =/= <. C , D >. ) )

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

Step

Hyp

Ref

Expression

 |-  ( A =/= C -> ( A =/= C \/ B =/= D ) )

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

1 2

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