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

Theorem prnebg 4212
 Description: A (proper) pair is not equal to another (maybe inproper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16-Jan-2018.)
Assertion
Ref Expression
prnebg

Proof of Theorem prnebg
StepHypRef Expression
1 prneimg 4211 . . 3
3 ioran 490 . . . . 5
4 ianor 488 . . . . . . 7
5 nne 2658 . . . . . . . 8
6 nne 2658 . . . . . . . 8
75, 6orbi12i 521 . . . . . . 7
84, 7bitri 249 . . . . . 6
9 ianor 488 . . . . . . 7
10 nne 2658 . . . . . . . 8
11 nne 2658 . . . . . . . 8
1210, 11orbi12i 521 . . . . . . 7
139, 12bitri 249 . . . . . 6
148, 13anbi12i 697 . . . . 5
153, 14bitri 249 . . . 4
16 anddi 870 . . . . 5
17 eqtr3 2485 . . . . . . . . . 10
18 eqneqall 2664 . . . . . . . . . 10
1917, 18syl 16 . . . . . . . . 9
20 preq12 4111 . . . . . . . . . 10
2120a1d 25 . . . . . . . . 9
2219, 21jaoi 379 . . . . . . . 8
23 preq12 4111 . . . . . . . . . . 11
24 prcom 4108 . . . . . . . . . . 11
2523, 24syl6eq 2514 . . . . . . . . . 10
2625a1d 25 . . . . . . . . 9
27 eqtr3 2485 . . . . . . . . . 10
2827, 18syl 16 . . . . . . . . 9
2926, 28jaoi 379 . . . . . . . 8
3022, 29jaoi 379 . . . . . . 7
3130com12 31 . . . . . 6
32313ad2ant3 1019 . . . . 5
3316, 32syl5bi 217 . . . 4
3415, 33syl5bi 217 . . 3
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  =/=wne 2652  {cpr 4031 This theorem is referenced by:  zlmodzxznm  33098 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032