Theorem funoprab

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

	Ref	Expression
Hypothesis	funoprab.1	$$⊢{\exists }^{*}z\phi$$
Assertion	funoprab	$$⊢\mathrm{Fun}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		funoprab.1	$$⊢{\exists }^{*}z\phi$$
2	1	gen2	$$⊢\forall x\forall y{\exists }^{*}z\phi$$
3		funoprabg	$$⊢\forall x\forall y{\exists }^{*}z\phi \to \mathrm{Fun}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
4	2 3	ax-mp	$$⊢\mathrm{Fun}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$