Metamath Proof Explorer


Theorem ex-ima

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

Ref Expression
Assertion ex-ima F = 2 6 3 9 B = 1 2 F B = 6

Proof

Step Hyp Ref Expression
1 df-ima F B = ran F B
2 ex-res F = 2 6 3 9 B = 1 2 F B = 2 6
3 2 rneqd F = 2 6 3 9 B = 1 2 ran F B = ran 2 6
4 1 3 syl5eq F = 2 6 3 9 B = 1 2 F B = ran 2 6
5 2ex 2 V
6 5 rnsnop ran 2 6 = 6
7 4 6 eqtrdi F = 2 6 3 9 B = 1 2 F B = 6