Theorem unass | index | src |

theorem unass (A B C: set): $ A u. B u. C == A u. (B u. C) $;
StepHypRefExpression
1 bitr4
(x e. A u. B u. C <-> x e. A u. B \/ x e. C) -> (x e. A u. (B u. C) <-> x e. A u. B \/ x e. C) -> (x e. A u. B u. C <-> x e. A u. (B u. C))
2 elun
x e. A u. B u. C <-> x e. A u. B \/ x e. C
3 1, 2 ax_mp
(x e. A u. (B u. C) <-> x e. A u. B \/ x e. C) -> (x e. A u. B u. C <-> x e. A u. (B u. C))
4 bitr4
(x e. A u. (B u. C) <-> x e. A \/ x e. B u. C) -> (x e. A u. B \/ x e. C <-> x e. A \/ x e. B u. C) -> (x e. A u. (B u. C) <-> x e. A u. B \/ x e. C)
5 elun
x e. A u. (B u. C) <-> x e. A \/ x e. B u. C
6 4, 5 ax_mp
(x e. A u. B \/ x e. C <-> x e. A \/ x e. B u. C) -> (x e. A u. (B u. C) <-> x e. A u. B \/ x e. C)
7 bitr4
(x e. A u. B \/ x e. C <-> x e. A \/ x e. B \/ x e. C) ->
  (x e. A \/ x e. B u. C <-> x e. A \/ x e. B \/ x e. C) ->
  (x e. A u. B \/ x e. C <-> x e. A \/ x e. B u. C)
8 elun
x e. A u. B <-> x e. A \/ x e. B
9 8 oreq1i
x e. A u. B \/ x e. C <-> x e. A \/ x e. B \/ x e. C
10 7, 9 ax_mp
(x e. A \/ x e. B u. C <-> x e. A \/ x e. B \/ x e. C) -> (x e. A u. B \/ x e. C <-> x e. A \/ x e. B u. C)
11 bitr4
(x e. A \/ x e. B u. C <-> x e. A \/ (x e. B \/ x e. C)) ->
  (x e. A \/ x e. B \/ x e. C <-> x e. A \/ (x e. B \/ x e. C)) ->
  (x e. A \/ x e. B u. C <-> x e. A \/ x e. B \/ x e. C)
12 elun
x e. B u. C <-> x e. B \/ x e. C
13 12 oreq2i
x e. A \/ x e. B u. C <-> x e. A \/ (x e. B \/ x e. C)
14 11, 13 ax_mp
(x e. A \/ x e. B \/ x e. C <-> x e. A \/ (x e. B \/ x e. C)) -> (x e. A \/ x e. B u. C <-> x e. A \/ x e. B \/ x e. C)
15 orass
x e. A \/ x e. B \/ x e. C <-> x e. A \/ (x e. B \/ x e. C)
16 14, 15 ax_mp
x e. A \/ x e. B u. C <-> x e. A \/ x e. B \/ x e. C
17 10, 16 ax_mp
x e. A u. B \/ x e. C <-> x e. A \/ x e. B u. C
18 6, 17 ax_mp
x e. A u. (B u. C) <-> x e. A u. B \/ x e. C
19 3, 18 ax_mp
x e. A u. B u. C <-> x e. A u. (B u. C)
20 19 eqri
A u. B u. C == A u. (B u. C)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8)