Metamath Proof Explorer


Theorem ovid

Description: The value of an operation class abstraction. (Contributed by NM, 16-May-1995) (Revised by David Abernethy, 19-Jun-2012)

Ref Expression
Hypotheses ovid.1 x R y S ∃! z φ
ovid.2 F = x y z | x R y S φ
Assertion ovid x R y S x F y = z φ

Proof

Step Hyp Ref Expression
1 ovid.1 x R y S ∃! z φ
2 ovid.2 F = x y z | x R y S φ
3 df-ov x F y = F x y
4 3 eqeq1i x F y = z F x y = z
5 1 fnoprab x y z | x R y S φ Fn x y | x R y S
6 2 fneq1i F Fn x y | x R y S x y z | x R y S φ Fn x y | x R y S
7 5 6 mpbir F Fn x y | x R y S
8 opabidw x y x y | x R y S x R y S
9 8 biimpri x R y S x y x y | x R y S
10 fnopfvb F Fn x y | x R y S x y x y | x R y S F x y = z x y z F
11 7 9 10 sylancr x R y S F x y = z x y z F
12 2 eleq2i x y z F x y z x y z | x R y S φ
13 oprabidw x y z x y z | x R y S φ x R y S φ
14 12 13 bitri x y z F x R y S φ
15 14 baib x R y S x y z F φ
16 11 15 bitrd x R y S F x y = z φ
17 4 16 syl5bb x R y S x F y = z φ