Theorem orvcval2

Description: Another way to express the value of the preimage mapping operator. (Contributed by Thierry Arnoux, 19-Jan-2017)

	Ref	Expression
Hypotheses	orvcval.1	|- ( ph -> Fun X )
	orvcval.2	|- ( ph -> X e. V )
	orvcval.3	|- ( ph -> A e. W )
Assertion	orvcval2	|- ( ph -> ( X oRVC R A ) = { z e. dom X | ( X ` z ) R A } )

Proof

Step	Hyp	Ref	Expression
1		orvcval.1	|- ( ph -> Fun X )
2		orvcval.2	|- ( ph -> X e. V )
3		orvcval.3	|- ( ph -> A e. W )
4	1 2 3	orvcval	|- ( ph -> ( X oRVC R A ) = ( `' X " { y | y R A } ) )
5		funfn	|- ( Fun X <-> X Fn dom X )
6	1 5	sylib	|- ( ph -> X Fn dom X )
7		fncnvima2	|- ( X Fn dom X -> ( `' X " { y | y R A } ) = { z e. dom X | ( X ` z ) e. { y | y R A } } )
8	6 7	syl	|- ( ph -> ( `' X " { y | y R A } ) = { z e. dom X | ( X ` z ) e. { y | y R A } } )
9		fvex	|- ( X ` z ) e. _V
10		breq1	|- ( y = ( X ` z ) -> ( y R A <-> ( X ` z ) R A ) )
11	9 10	elab	|- ( ( X ` z ) e. { y | y R A } <-> ( X ` z ) R A )
12	11	rabbii	|- { z e. dom X | ( X ` z ) e. { y | y R A } } = { z e. dom X | ( X ` z ) R A }
13	12	a1i	|- ( ph -> { z e. dom X | ( X ` z ) e. { y | y R A } } = { z e. dom X | ( X ` z ) R A } )
14	4 8 13	3eqtrd	|- ( ph -> ( X oRVC R A ) = { z e. dom X | ( X ` z ) R A } )