Metamath Proof Explorer

Theorem prneimg2

Description: Two pairs are not equal if their counterparts are not equal. (Contributed by AV, 5-Sep-2025)

Ref Expression
Assertion prneimg2 
|- ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } =/= { C , D } <-> ( ( A =/= C \/ B =/= D ) /\ ( A =/= D \/ B =/= C ) ) ) )

Proof

Step Hyp Ref Expression
1 preq12bg 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
2 1 necon3abid 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } =/= { C , D } <-> -. ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
3 ioran 
 |-  ( -. ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) <-> ( -. ( A = C /\ B = D ) /\ -. ( A = D /\ B = C ) ) )
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 ianor 
 |-  ( -. ( A = D /\ B = C ) <-> ( -. A = D \/ -. B = C ) )
10 df-ne 
 |-  ( A =/= D <-> -. A = D )
11 df-ne 
 |-  ( B =/= C <-> -. B = C )
12 10 11 orbi12i 
 |-  ( ( A =/= D \/ B =/= C ) <-> ( -. A = D \/ -. B = C ) )
13 9 12 bitr4i 
 |-  ( -. ( A = D /\ B = C ) <-> ( A =/= D \/ B =/= C ) )
14 8 13 anbi12i 
 |-  ( ( -. ( A = C /\ B = D ) /\ -. ( A = D /\ B = C ) ) <-> ( ( A =/= C \/ B =/= D ) /\ ( A =/= D \/ B =/= C ) ) )
15 3 14 bitri 
 |-  ( -. ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) <-> ( ( A =/= C \/ B =/= D ) /\ ( A =/= D \/ B =/= C ) ) )
16 2 15 bitrdi 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } =/= { C , D } <-> ( ( A =/= C \/ B =/= D ) /\ ( A =/= D \/ B =/= C ) ) ) )