Theorem dmun ≪ | index | src | ≫ 

theorem dmun (A B: set): $ Dom (A u. B) == Dom A u. Dom B $;
StepHypRefExpression
1 bitr4 
(a1 e. Dom (A u. B) <-> E. a2 a1, a2 e. A u. B) -> (a1 e. Dom A u. Dom B <-> E. a2 a1, a2 e. A u. B) -> (a1 e. Dom (A u. B) <-> a1 e. Dom A u. Dom B)
2 eldm 
a1 e. Dom (A u. B) <-> E. a2 a1, a2 e. A u. B
3 1, 2 ax_mp 
(a1 e. Dom A u. Dom B <-> E. a2 a1, a2 e. A u. B) -> (a1 e. Dom (A u. B) <-> a1 e. Dom A u. Dom B)
4 bitr4 
(a1 e. Dom A u. Dom B <-> a1 e. Dom A \/ a1 e. Dom B) ->
  (E. a2 a1, a2 e. A u. B <-> a1 e. Dom A \/ a1 e. Dom B) ->
  (a1 e. Dom A u. Dom B <-> E. a2 a1, a2 e. A u. B)
5 elun 
a1 e. Dom A u. Dom B <-> a1 e. Dom A \/ a1 e. Dom B
6 4, 5 ax_mp 
(E. a2 a1, a2 e. A u. B <-> a1 e. Dom A \/ a1 e. Dom B) -> (a1 e. Dom A u. Dom B <-> E. a2 a1, a2 e. A u. B)
7 bitr4 
(E. a2 a1, a2 e. A u. B <-> E. a2 (a1, a2 e. A \/ a1, a2 e. B)) ->
  (a1 e. Dom A \/ a1 e. Dom B <-> E. a2 (a1, a2 e. A \/ a1, a2 e. B)) ->
  (E. a2 a1, a2 e. A u. B <-> a1 e. Dom A \/ a1 e. Dom B)
8 elun 
a1, a2 e. A u. B <-> a1, a2 e. A \/ a1, a2 e. B
9 8 exeqi 
E. a2 a1, a2 e. A u. B <-> E. a2 (a1, a2 e. A \/ a1, a2 e. B)
10 7, 9 ax_mp 
(a1 e. Dom A \/ a1 e. Dom B <-> E. a2 (a1, a2 e. A \/ a1, a2 e. B)) -> (E. a2 a1, a2 e. A u. B <-> a1 e. Dom A \/ a1 e. Dom B)
11 bitr4 
(a1 e. Dom A \/ a1 e. Dom B <-> E. a2 a1, a2 e. A \/ E. a2 a1, a2 e. B) ->
  (E. a2 (a1, a2 e. A \/ a1, a2 e. B) <-> E. a2 a1, a2 e. A \/ E. a2 a1, a2 e. B) ->
  (a1 e. Dom A \/ a1 e. Dom B <-> E. a2 (a1, a2 e. A \/ a1, a2 e. B))
12 oreq 
(a1 e. Dom A <-> E. a2 a1, a2 e. A) -> (a1 e. Dom B <-> E. a2 a1, a2 e. B) -> (a1 e. Dom A \/ a1 e. Dom B <-> E. a2 a1, a2 e. A \/ E. a2 a1, a2 e. B)
13 eldm 
a1 e. Dom A <-> E. a2 a1, a2 e. A
14 12, 13 ax_mp 
(a1 e. Dom B <-> E. a2 a1, a2 e. B) -> (a1 e. Dom A \/ a1 e. Dom B <-> E. a2 a1, a2 e. A \/ E. a2 a1, a2 e. B)
15 eldm 
a1 e. Dom B <-> E. a2 a1, a2 e. B
16 14, 15 ax_mp 
a1 e. Dom A \/ a1 e. Dom B <-> E. a2 a1, a2 e. A \/ E. a2 a1, a2 e. B
17 11, 16 ax_mp 
(E. a2 (a1, a2 e. A \/ a1, a2 e. B) <-> E. a2 a1, a2 e. A \/ E. a2 a1, a2 e. B) -> (a1 e. Dom A \/ a1 e. Dom B <-> E. a2 (a1, a2 e. A \/ a1, a2 e. B))
18 exor 
E. a2 (a1, a2 e. A \/ a1, a2 e. B) <-> E. a2 a1, a2 e. A \/ E. a2 a1, a2 e. B
19 17, 18 ax_mp 
a1 e. Dom A \/ a1 e. Dom B <-> E. a2 (a1, a2 e. A \/ a1, a2 e. B)
20 10, 19 ax_mp 
E. a2 a1, a2 e. A u. B <-> a1 e. Dom A \/ a1 e. Dom B
21 6, 20 ax_mp 
a1 e. Dom A u. Dom B <-> E. a2 a1, a2 e. A u. B
22 3, 21 ax_mp 
a1 e. Dom (A u. B) <-> a1 e. Dom A u. Dom B
23 22 ax_gen 
A. a1 (a1 e. Dom (A u. B) <-> a1 e. Dom A u. Dom B)
24 23 conv eqs 
Dom (A u. B) == Dom A u. Dom B

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), axs_the (theid, the0), axs_peano (peano2, addeq, muleq)