Metamath Proof Explorer

Theorem opthneg

Description: Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018)

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

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( <. A , B >. =/= <. C , D >. <-> -. <. A , B >. = <. C , D >. )
2 opthg 
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) )
3 2 notbid 
 |-  ( ( A e. V /\ B e. W ) -> ( -. <. A , B >. = <. C , D >. <-> -. ( A = C /\ B = D ) ) )
4 ianor 
 |-  ( -. ( A = C /\ B = D ) <-> ( -. A = C \/ -. B = D ) )
5 df-ne 
 |-  ( A =/= C <-> -. A = C )
6 df-ne 
 |-  ( B =/= D <-> -. B = D )
7 5 6 orbi12i 
 |-  ( ( A =/= C \/ B =/= D ) <-> ( -. A = C \/ -. B = D ) )
8 4 7 bitr4i 
 |-  ( -. ( A = C /\ B = D ) <-> ( A =/= C \/ B =/= D ) )
9 3 8 bitrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( -. <. A , B >. = <. C , D >. <-> ( A =/= C \/ B =/= D ) ) )
10 1 9 bitrid 
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. =/= <. C , D >. <-> ( A =/= C \/ B =/= D ) ) )