Metamath Proof Explorer


Theorem fvelrnb

Description: A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995)

Ref Expression
Assertion fvelrnb F Fn A B ran F x A F x = B

Proof

Step Hyp Ref Expression
1 fnrnfv F Fn A ran F = y | x A y = F x
2 1 eleq2d F Fn A B ran F B y | x A y = F x
3 fvex F x V
4 eleq1 F x = B F x V B V
5 3 4 mpbii F x = B B V
6 5 rexlimivw x A F x = B B V
7 eqeq1 y = B y = F x B = F x
8 eqcom B = F x F x = B
9 7 8 bitrdi y = B y = F x F x = B
10 9 rexbidv y = B x A y = F x x A F x = B
11 6 10 elab3 B y | x A y = F x x A F x = B
12 2 11 bitrdi F Fn A B ran F x A F x = B