Metamath Proof Explorer


Theorem ex-rn

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

Ref Expression
Assertion ex-rn F = 2 6 3 9 ran F = 6 9

Proof

Step Hyp Ref Expression
1 rneq F = 2 6 3 9 ran F = ran 2 6 3 9
2 df-pr 2 6 3 9 = 2 6 3 9
3 2 rneqi ran 2 6 3 9 = ran 2 6 3 9
4 rnun ran 2 6 3 9 = ran 2 6 ran 3 9
5 2nn 2
6 5 elexi 2 V
7 6 rnsnop ran 2 6 = 6
8 3nn 3
9 8 elexi 3 V
10 9 rnsnop ran 3 9 = 9
11 7 10 uneq12i ran 2 6 ran 3 9 = 6 9
12 df-pr 6 9 = 6 9
13 11 12 eqtr4i ran 2 6 ran 3 9 = 6 9
14 3 4 13 3eqtri ran 2 6 3 9 = 6 9
15 1 14 eqtrdi F = 2 6 3 9 ran F = 6 9