Theorem rightval

Description: The value of the right options function. (Contributed by Scott Fenton, 6-Aug-2024)

	Ref	Expression
Assertion	rightval	|- ( A e. No -> ( _R ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A

Proof

Step	Hyp	Ref	Expression
1		2fveq3	|- ( y = A -> ( _Old ` ( bday ` y ) ) = ( _Old ` ( bday ` A ) ) )
2		breq1	|- ( y = A -> ( y A
3	1 2	rabeqbidv	|- ( y = A -> { x e. ( _Old ` ( bday ` y ) ) | y
4		df-right	|- _R = ( y e. No |-> { x e. ( _Old ` ( bday ` y ) ) | y
5		fvex	|- ( _Old ` ( bday ` A ) ) e. _V
6	5	rabex	|- { x e. ( _Old ` ( bday ` A ) ) | A
7	3 4 6	fvmpt	|- ( A e. No -> ( _R ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A