Theorem 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	⊢ ( ∀ 𝑥 ∀ 𝑦 ∃* 𝑧 𝜑 → Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		mosubopt	⊢ ( ∀ 𝑥 ∀ 𝑦 ∃* 𝑧 𝜑 → ∃* 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
2	1	alrimiv	⊢ ( ∀ 𝑥 ∀ 𝑦 ∃* 𝑧 𝜑 → ∀ 𝑤 ∃* 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
3		dfoprab2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
4	3	funeqi	⊢ ( Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } )
5		funopab	⊢ ( Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ↔ ∀ 𝑤 ∃* 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
6	4 5	bitr2i	⊢ ( ∀ 𝑤 ∃* 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } )
7	2 6	sylib	⊢ ( ∀ 𝑥 ∀ 𝑦 ∃* 𝑧 𝜑 → Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } )