Theorem ovidi

Description: The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	ovidi.2	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃* 𝑧 𝜑 )
	ovidi.3	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) }
Assertion	ovidi	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( 𝜑 → ( 𝑥 𝐹 𝑦 ) = 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		ovidi.2	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃* 𝑧 𝜑 )
2		ovidi.3	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) }
3		moanimv	⊢ ( ∃* 𝑧 ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃* 𝑧 𝜑 ) )
4	1 3	mpbir	⊢ ∃* 𝑧 ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 )
5	4 2	ovidig	⊢ ( ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) → ( 𝑥 𝐹 𝑦 ) = 𝑧 )
6	5	ex	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( 𝜑 → ( 𝑥 𝐹 𝑦 ) = 𝑧 ) )