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

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 | ph } = { y } }
Assertion opabiotafun 
|- Fun F

Proof

Step Hyp Ref Expression
1 opabiota.1 
 |-  F = { <. x , y >. | { y | ph } = { y } }
2 funopab 
 |-  ( Fun { <. x , y >. | { y | ph } = { y } } <-> A. x E* y { y | ph } = { y } )
3 mo2icl 
 |-  ( A. z ( { y | ph } = { z } -> z = U. { y | ph } ) -> E* z { y | ph } = { z } )
4 unieq 
 |-  ( { y | ph } = { z } -> U. { y | ph } = U. { z } )
5 unisnv 
 |-  U. { z } = z
6 4 5 eqtr2di 
 |-  ( { y | ph } = { z } -> z = U. { y | ph } )
7 3 6 mpg 
 |-  E* z { y | ph } = { z }
8 nfv 
 |-  F/ z { y | ph } = { y }
9 nfab1 
 |-  F/_ y { y | ph }
10 9 nfeq1 
 |-  F/ y { y | ph } = { z }
11 sneq 
 |-  ( y = z -> { y } = { z } )
12 11 eqeq2d 
 |-  ( y = z -> ( { y | ph } = { y } <-> { y | ph } = { z } ) )
13 8 10 12 cbvmow 
 |-  ( E* y { y | ph } = { y } <-> E* z { y | ph } = { z } )
14 7 13 mpbir 
 |-  E* y { y | ph } = { y }
15 2 14 mpgbir 
 |-  Fun { <. x , y >. | { y | ph } = { y } }
16 1 funeqi 
 |-  ( Fun F <-> Fun { <. x , y >. | { y | ph } = { y } } )
17 15 16 mpbir 
 |-  Fun F