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

Metamath Proof Explorer

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 \cup G) \to \exists^{*} y x F y$

Proof

Step	Hyp	Ref	Expression
1		funmo	$⊢ Fun (F \cup G) \to \exists^{*} y x (F \cup G) y$
2		orc	$⊢ x F y \to (x F y \lor x G y)$
3		brun	$⊢ x (F \cup G) y \leftrightarrow (x F y \lor x G y)$
4	2 3	sylibr	$⊢ x F y \to x (F \cup G) y$
5	4	moimi	$⊢ \exists^{} y x (F \cup G) y \to \exists^{} y x F y$
6	1 5	syl	$⊢ Fun (F \cup G) \to \exists^{*} y x F y$