Theorem rnun ≪ | index | src | ≫ 

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