Theorem fun2d

Description: The union of functions with disjoint domains is a function, deduction version of fun2 . (Contributed by AV, 11-Oct-2020) (Revised by AV, 24-Oct-2021)

	Ref	Expression
Hypotheses	fun2d.f	$$⊢\phi \to F:A⟶C$$
	fun2d.g	$$⊢\phi \to G:B⟶C$$
	fun2d.i	$$⊢\phi \to A\cap B=\varnothing$$
Assertion	fun2d	$$⊢\phi \to \left(F\cup G\right):A\cup B⟶C$$

Proof

Step	Hyp	Ref	Expression
1		fun2d.f	$$⊢\phi \to F:A⟶C$$
2		fun2d.g	$$⊢\phi \to G:B⟶C$$
3		fun2d.i	$$⊢\phi \to A\cap B=\varnothing$$
4		fun2	$$⊢\left(\left(F:A⟶C\wedge G:B⟶C\right)\wedge A\cap B=\varnothing \right)\to \left(F\cup G\right):A\cup B⟶C$$
5	1 2 3 4	syl21anc	$$⊢\phi \to \left(F\cup G\right):A\cup B⟶C$$