Theorem map_union_eq_rngs

Proof
01. 1 ⊢ map f X1 Y, hypo.
02. 2 ⊢ map g X2 Y, hypo.
03. 3 ⊢ X1 ∩ X2 = ∅, hypo.
04. 1, 2, 3 ⊢ map (f ∪ g) (X1 ∪ X2) (Y ∪ Y), map_union 1 2 3.
05. ⊢ Y ∪ Y = Y, union_idem.
06. 1, 2, 3 ⊢ map (f ∪ g) (X1 ∪ X2) Y, eq_subst 5 4,
  P u ↔ map (f ∪ g) (X1 ∪ X2) u.
map_union_eq_rngs. ⊢ map f X1 Y → map g X2 Y → X1 ∩ X2 = ∅ →
  map (f ∪ g) (X1 ∪ X2) Y, subj_intro_iii 6.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.