Theorem fununmo

Description: If the union of classes is a function, there is at most one element in relation to an arbitrary element regarding one of these classes. (Contributed by AV, 18-Jul-2019)

	Ref	Expression
Assertion	fununmo	⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → ∃* 𝑦 𝑥 𝐹 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		funmo	⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → ∃* 𝑦 𝑥 ( 𝐹 ∪ 𝐺 ) 𝑦 )
2		orc	⊢ ( 𝑥 𝐹 𝑦 → ( 𝑥 𝐹 𝑦 ∨ 𝑥 𝐺 𝑦 ) )
3		brun	⊢ ( 𝑥 ( 𝐹 ∪ 𝐺 ) 𝑦 ↔ ( 𝑥 𝐹 𝑦 ∨ 𝑥 𝐺 𝑦 ) )
4	2 3	sylibr	⊢ ( 𝑥 𝐹 𝑦 → 𝑥 ( 𝐹 ∪ 𝐺 ) 𝑦 )
5	4	moimi	⊢ ( ∃* 𝑦 𝑥 ( 𝐹 ∪ 𝐺 ) 𝑦 → ∃* 𝑦 𝑥 𝐹 𝑦 )
6	1 5	syl	⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → ∃* 𝑦 𝑥 𝐹 𝑦 )