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 = x y z | φ
Assertion ovidig φ x F y = z

Proof

Step Hyp Ref Expression
1 ovidig.1 * z φ
2 ovidig.2 F = x y z | φ
3 df-ov x F y = F x y
4 1 funoprab Fun x y z | φ
5 2 funeqi Fun F Fun x y z | φ
6 4 5 mpbir Fun F
7 oprabidw x y z x y z | φ φ
8 7 biimpri φ x y z x y z | φ
9 8 2 eleqtrrdi φ x y z F
10 funopfv Fun F x y z F F x y = z
11 6 9 10 mpsyl φ F x y = z
12 3 11 eqtrid φ x F y = z