Metamath Proof Explorer


Theorem rnun

Description: Distributive law for range over union. Theorem 8 of Suppes p. 60. (Contributed by NM, 24-Mar-1998)

Ref Expression
Assertion rnun ran A B = ran A ran B

Proof

Step Hyp Ref Expression
1 cnvun A B -1 = A -1 B -1
2 1 dmeqi dom A B -1 = dom A -1 B -1
3 dmun dom A -1 B -1 = dom A -1 dom B -1
4 2 3 eqtri dom A B -1 = dom A -1 dom B -1
5 df-rn ran A B = dom A B -1
6 df-rn ran A = dom A -1
7 df-rn ran B = dom B -1
8 6 7 uneq12i ran A ran B = dom A -1 dom B -1
9 4 5 8 3eqtr4i ran A B = ran A ran B