Theorem fnoprab

Description: Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995)

	Ref	Expression
Hypothesis	fnoprab.1	⊢ ( 𝜑 → ∃! 𝑧 𝜓 )
Assertion	fnoprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		fnoprab.1	⊢ ( 𝜑 → ∃! 𝑧 𝜓 )
2	1	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 )
3		fnoprabg	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
4	2 3	ax-mp	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }