This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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