Metamath Proof Explorer


Theorem opabiotafun

Description: Define a function whose value is "the unique y such that ph ( x , y ) ". (Contributed by NM, 19-May-2015)

Ref Expression
Hypothesis opabiota.1 F = x y | y | φ = y
Assertion opabiotafun Fun F

Proof

Step Hyp Ref Expression
1 opabiota.1 F = x y | y | φ = y
2 funopab Fun x y | y | φ = y x * y y | φ = y
3 mo2icl z y | φ = z z = y | φ * z y | φ = z
4 unieq y | φ = z y | φ = z
5 vex z V
6 5 unisn z = z
7 4 6 syl6req y | φ = z z = y | φ
8 3 7 mpg * z y | φ = z
9 nfv z y | φ = y
10 nfab1 _ y y | φ
11 10 nfeq1 y y | φ = z
12 sneq y = z y = z
13 12 eqeq2d y = z y | φ = y y | φ = z
14 9 11 13 cbvmow * y y | φ = y * z y | φ = z
15 8 14 mpbir * y y | φ = y
16 2 15 mpgbir Fun x y | y | φ = y
17 1 funeqi Fun F Fun x y | y | φ = y
18 16 17 mpbir Fun F