funoprabg

Description: "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007)

		Ref	Expression
	Assertion	funoprabg	$⊢ \forall x \forall y \exists^{*} z φ \to Fun \{⟨⟨x, y⟩, z⟩ \| φ\}$

Step	Hyp	Ref	Expression
1		mosubopt	$⊢ \forall x \forall y \exists^{} z φ \to \exists^{} z \exists x \exists y (w = ⟨x, y⟩ \land φ)$
2	1	alrimiv	$⊢ \forall x \forall y \exists^{} z φ \to \forall w \exists^{} z \exists x \exists y (w = ⟨x, y⟩ \land φ)$
3		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
4	3	funeqi	$⊢ Fun \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow Fun \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
5		funopab	$⊢ Fun \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} \leftrightarrow \forall w \exists^{*} z \exists x \exists y (w = ⟨x, y⟩ \land φ)$
6	4 5	bitr2i	$⊢ \forall w \exists^{*} z \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow Fun \{⟨⟨x, y⟩, z⟩ \| φ\}$
7	2 6	sylib	$⊢ \forall x \forall y \exists^{*} z φ \to Fun \{⟨⟨x, y⟩, z⟩ \| φ\}$

Metamath Proof Explorer