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 ( F u. G ) -> E* y x F y )

Proof

Step	Hyp	Ref	Expression
1		funmo	|- ( Fun ( F u. G ) -> E* y x ( F u. G ) y )
2		orc	|- ( x F y -> ( x F y \/ x G y ) )
3		brun	|- ( x ( F u. G ) y <-> ( x F y \/ x G y ) )
4	2 3	sylibr	|- ( x F y -> x ( F u. G ) y )
5	4	moimi	|- ( E* y x ( F u. G ) y -> E* y x F y )
6	1 5	syl	|- ( Fun ( F u. G ) -> E* y x F y )