Metamath Proof Explorer

Theorem prneimg

Description: Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017)

Ref Expression
Assertion prneimg ⊢A∈U∧B∈V∧C∈X∧D∈Y→A≠C∧A≠D∨B≠C∧B≠D→AB≠CD

Proof

Step Hyp Ref Expression
1 preq12bg ⊢A∈U∧B∈V∧C∈X∧D∈Y→AB=CD↔A=C∧B=D∨A=D∧B=C
2 orddi ⊢A=C∧B=D∨A=D∧B=C↔A=C∨A=D∧A=C∨B=C∧B=D∨A=D∧B=D∨B=C
3 simpll ⊢A=C∨A=D∧A=C∨B=C∧B=D∨A=D∧B=D∨B=C→A=C∨A=D
4 pm1.4 ⊢B=D∨B=C→B=C∨B=D
5 4 ad2antll ⊢A=C∨A=D∧A=C∨B=C∧B=D∨A=D∧B=D∨B=C→B=C∨B=D
6 3 5 jca ⊢A=C∨A=D∧A=C∨B=C∧B=D∨A=D∧B=D∨B=C→A=C∨A=D∧B=C∨B=D
7 2 6 sylbi ⊢A=C∧B=D∨A=D∧B=C→A=C∨A=D∧B=C∨B=D
8 1 7 biimtrdi ⊢A∈U∧B∈V∧C∈X∧D∈Y→AB=CD→A=C∨A=D∧B=C∨B=D
9 ianor ⊢¬A≠C∧A≠D↔¬A≠C∨¬A≠D
10 nne ⊢¬A≠C↔A=C
11 nne ⊢¬A≠D↔A=D
12 10 11 orbi12i ⊢¬A≠C∨¬A≠D↔A=C∨A=D
13 9 12 bitr2i ⊢A=C∨A=D↔¬A≠C∧A≠D
14 ianor ⊢¬B≠C∧B≠D↔¬B≠C∨¬B≠D
15 nne ⊢¬B≠C↔B=C
16 nne ⊢¬B≠D↔B=D
17 15 16 orbi12i ⊢¬B≠C∨¬B≠D↔B=C∨B=D
18 14 17 bitr2i ⊢B=C∨B=D↔¬B≠C∧B≠D
19 13 18 anbi12i ⊢A=C∨A=D∧B=C∨B=D↔¬A≠C∧A≠D∧¬B≠C∧B≠D
20 8 19 imbitrdi ⊢A∈U∧B∈V∧C∈X∧D∈Y→AB=CD→¬A≠C∧A≠D∧¬B≠C∧B≠D
21 pm4.56 ⊢¬A≠C∧A≠D∧¬B≠C∧B≠D↔¬A≠C∧A≠D∨B≠C∧B≠D
22 20 21 imbitrdi ⊢A∈U∧B∈V∧C∈X∧D∈Y→AB=CD→¬A≠C∧A≠D∨B≠C∧B≠D
23 22 necon2ad ⊢A∈U∧B∈V∧C∈X∧D∈Y→A≠C∧A≠D∨B≠C∧B≠D→AB≠CD