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 → A B ≠ C D

Proof

Step Hyp Ref Expression
1 preq12bg ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ D ∈ Y → A B = C D ↔ 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 syl6bi ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ D ∈ Y → A B = C D → 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 syl6ib ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ D ∈ Y → A B = C D → ¬ 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 syl6ib ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ D ∈ Y → A B = C D → ¬ 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 → A B ≠ C D