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	$$⊢\mathrm{Fun}\left(F\cup G\right)\to {\exists }^{*}yxFy$$

Proof

Step	Hyp	Ref	Expression
1		funmo	$$⊢\mathrm{Fun}\left(F\cup G\right)\to {\exists }^{*}yx\left(F\cup G\right)y$$
2		orc	$$⊢xFy\to \left(xFy\vee xGy\right)$$
3		brun	$$⊢x\left(F\cup G\right)y\leftrightarrow \left(xFy\vee xGy\right)$$
4	2 3	sylibr	$$⊢xFy\to x\left(F\cup G\right)y$$
5	4	moimi	$$⊢{\exists }^{*}yx\left(F\cup G\right)y\to {\exists }^{*}yxFy$$
6	1 5	syl	$$⊢\mathrm{Fun}\left(F\cup G\right)\to {\exists }^{*}yxFy$$