Metamath Proof Explorer


Theorem ex-fv

Description: Example for df-fv . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion ex-fv F = 2 6 3 9 F 3 = 9

Proof

Step Hyp Ref Expression
1 fveq1 F = 2 6 3 9 F 3 = 2 6 3 9 3
2 2re 2
3 2lt3 2 < 3
4 2 3 ltneii 2 3
5 3ex 3 V
6 9re 9
7 6 elexi 9 V
8 5 7 fvpr2 2 3 2 6 3 9 3 = 9
9 4 8 ax-mp 2 6 3 9 3 = 9
10 1 9 eqtrdi F = 2 6 3 9 F 3 = 9