This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnund

Description: The union of two functions with disjoint domains, a deduction version. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses fnund.1 ⊢ φ → F Fn A
fnund.2 ⊢ φ → G Fn B
fnund.3 ⊢ φ → A ∩ B = ∅
Assertion fnund ⊢ φ → F ∪ G Fn A ∪ B

Proof

Step Hyp Ref Expression
1 fnund.1 ⊢ φ → F Fn A
2 fnund.2 ⊢ φ → G Fn B
3 fnund.3 ⊢ φ → A ∩ B = ∅
4 fnun ⊢ F Fn A ∧ G Fn B ∧ A ∩ B = ∅ → F ∪ G Fn A ∪ B
5 1 2 3 4 syl21anc ⊢ φ → F ∪ G Fn A ∪ B