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 *zφ
ovidig.2 F=xyz|φ
Assertion ovidig φxFy=z

Proof

Step Hyp Ref Expression
1 ovidig.1 *zφ
2 ovidig.2 F=xyz|φ
3 df-ov xFy=Fxy
4 1 funoprab Funxyz|φ
5 2 funeqi FunFFunxyz|φ
6 4 5 mpbir FunF
7 oprabidw xyzxyz|φφ
8 7 biimpri φxyzxyz|φ
9 8 2 eleqtrrdi φxyzF
10 funopfv FunFxyzFFxy=z
11 6 9 10 mpsyl φFxy=z
12 3 11 eqtrid φxFy=z