Metamath Proof Explorer

Theorem opth2neg

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

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

Step	Hyp	Ref	Expression
1		olc	\|- ( B =/= D -> ( 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 ) -> ( B =/= D -> <. A , B >. =/= <. C , D >. ) )

Step

Hyp

Ref

Expression

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