Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ddifstab Unicode version

Theorem ddifstab 3172
 Description: A class is equal to its double complement if and only if it is stable (that is, membership in it is a stable property). (Contributed by BJ, 12-Dec-2021.)
Assertion
Ref Expression
ddifstab STAB
Distinct variable group:   ,

Proof of Theorem ddifstab
StepHypRef Expression
1 dfcleq 2107 . 2
2 eldif 3044 . . . . . . 7
3 vex 2658 . . . . . . . 8
43biantrur 299 . . . . . . 7
5 eldif 3044 . . . . . . . . 9
63biantrur 299 . . . . . . . . 9
75, 6bitr4i 186 . . . . . . . 8
87notbii 640 . . . . . . 7
92, 4, 83bitr2i 207 . . . . . 6
109bibi1i 227 . . . . 5
11 bi1 117 . . . . . 6
12 id 19 . . . . . . 7
13 notnot 601 . . . . . . 7
1412, 13impbid1 141 . . . . . 6
1511, 14impbii 125 . . . . 5
1610, 15bitri 183 . . . 4
17 df-stab 799 . . . 4 STAB
1816, 17bitr4i 186 . . 3 STAB
1918albii 1427 . 2 STAB
201, 19bitri 183 1 STAB
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wb 104  STAB wstab 798  wal 1310   wceq 1312   wcel 1461  cvv 2655   cdif 3032 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095 This theorem depends on definitions:  df-bi 116  df-stab 799  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-dif 3037 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator