Theorem ovidig

Description: The value of an operation class abstraction. Compare ovidi . The condition ( x e. R /\ y e. S ) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	ovidig.1	⊢ ∃* 𝑧 𝜑
	ovidig.2	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
Assertion	ovidig	⊢ ( 𝜑 → ( 𝑥 𝐹 𝑦 ) = 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		ovidig.1	⊢ ∃* 𝑧 𝜑
2		ovidig.2	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
3		df-ov	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4	1	funoprab	⊢ Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
5	2	funeqi	⊢ ( Fun 𝐹 ↔ Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } )
6	4 5	mpbir	⊢ Fun 𝐹
7		oprabidw	⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜑 )
8	7	biimpri	⊢ ( 𝜑 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } )
9	8 2	eleqtrrdi	⊢ ( 𝜑 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹 )
10		funopfv	⊢ ( Fun 𝐹 → ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹 → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) )
11	6 9 10	mpsyl	⊢ ( 𝜑 → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 )
12	3 11	syl5eq	⊢ ( 𝜑 → ( 𝑥 𝐹 𝑦 ) = 𝑧 )