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	⊢ ∃* 𝑧 𝜑
Assertion	funoprab	⊢ Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		funoprab.1	⊢ ∃* 𝑧 𝜑
2	1	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ∃* 𝑧 𝜑
3		funoprabg	⊢ ( ∀ 𝑥 ∀ 𝑦 ∃* 𝑧 𝜑 → Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } )
4	2 3	ax-mp	⊢ Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }