Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prneimg Structured version   Unicode version

Theorem prneimg 4152
 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.)
Assertion
Ref Expression
prneimg

Proof of Theorem prneimg
StepHypRef Expression
1 preq12bg 4150 . . . . 5
2 orddi 870 . . . . . 6
3 simpll 752 . . . . . . 7
4 pm1.4 384 . . . . . . . 8
54ad2antll 727 . . . . . . 7
63, 5jca 530 . . . . . 6
72, 6sylbi 195 . . . . 5
81, 7syl6bi 228 . . . 4
9 ianor 486 . . . . . 6
10 nne 2604 . . . . . . 7
11 nne 2604 . . . . . . 7
1210, 11orbi12i 519 . . . . . 6
139, 12bitr2i 250 . . . . 5
14 ianor 486 . . . . . 6
15 nne 2604 . . . . . . 7
16 nne 2604 . . . . . . 7
1715, 16orbi12i 519 . . . . . 6
1814, 17bitr2i 250 . . . . 5
1913, 18anbi12i 695 . . . 4
208, 19syl6ib 226 . . 3
21 pm4.56 493 . . 3
2220, 21syl6ib 226 . 2