Theorem elorvc

Description: Elementhood of a preimage. (Contributed by Thierry Arnoux, 21-Jan-2017)

	Ref	Expression
Hypotheses	orvcval.1	|- ( ph -> Fun X )
	orvcval.2	|- ( ph -> X e. V )
	orvcval.3	|- ( ph -> A e. W )
Assertion	elorvc	|- ( ( ph /\ z e. dom X ) -> ( z e. ( X oRVC R A ) <-> ( 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	orvcval2	|- ( ph -> ( X oRVC R A ) = { z e. dom X | ( X ` z ) R A } )
5	4	eleq2d	|- ( ph -> ( z e. ( X oRVC R A ) <-> z e. { z e. dom X | ( X ` z ) R A } ) )
6		rabid	|- ( z e. { z e. dom X | ( X ` z ) R A } <-> ( z e. dom X /\ ( X ` z ) R A ) )
7	5 6	bitrdi	|- ( ph -> ( z e. ( X oRVC R A ) <-> ( z e. dom X /\ ( X ` z ) R A ) ) )
8	7	baibd	|- ( ( ph /\ z e. dom X ) -> ( z e. ( X oRVC R A ) <-> ( X ` z ) R A ) )