infeu

	Ref	Expression
Hypotheses	infmo.1	$⊢ φ \to R Or A$
	infeu.2	$⊢ φ \to \exists x \in A (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y))$
Assertion	infeu	$⊢ φ \to \exists! x \in A (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y))$

Step	Hyp	Ref	Expression
1		infmo.1	$⊢ φ \to R Or A$
2		infeu.2	$⊢ φ \to \exists x \in A (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y))$
3	1	infmo	$⊢ φ \to \exists^{*} x \in A (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y))$
4		reu5	$⊢ \exists! x \in A (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y)) \leftrightarrow (\exists x \in A (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y)) \land \exists^{*} x \in A (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y)))$
5	2 3 4	sylanbrc	$⊢ φ \to \exists! x \in A (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y))$

Metamath Proof Explorer