Metamath Proof Explorer


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 ( ( 𝑥𝑅𝑦𝑆 ) → ( 𝜑 → ( 𝑥 𝐹 𝑦 ) = 𝑧 ) )