Metamath Proof Explorer


Theorem ovelrn

Description: A member of an operation's range is a value of the operation. (Contributed by NM, 7-Feb-2007) (Revised by Mario Carneiro, 30-Jan-2014)

Ref Expression
Assertion ovelrn F Fn A × B C ran F x A y B C = x F y

Proof

Step Hyp Ref Expression
1 fnrnov F Fn A × B ran F = z | x A y B z = x F y
2 1 eleq2d F Fn A × B C ran F C z | x A y B z = x F y
3 ovex x F y V
4 eleq1 C = x F y C V x F y V
5 3 4 mpbiri C = x F y C V
6 5 rexlimivw y B C = x F y C V
7 6 rexlimivw x A y B C = x F y C V
8 eqeq1 z = C z = x F y C = x F y
9 8 2rexbidv z = C x A y B z = x F y x A y B C = x F y
10 7 9 elab3 C z | x A y B z = x F y x A y B C = x F y
11 2 10 bitrdi F Fn A × B C ran F x A y B C = x F y