Metamath Proof Explorer


Theorem fnasrn

Description: A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013) (Proof shortened by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis dfmpt.1 B V
Assertion fnasrn x A B = ran x A x B

Proof

Step Hyp Ref Expression
1 dfmpt.1 B V
2 1 dfmpt x A B = x A x B
3 eqid x A x B = x A x B
4 3 rnmpt ran x A x B = y | x A y = x B
5 velsn y x B y = x B
6 5 rexbii x A y x B x A y = x B
7 6 abbii y | x A y x B = y | x A y = x B
8 4 7 eqtr4i ran x A x B = y | x A y x B
9 df-iun x A x B = y | x A y x B
10 8 9 eqtr4i ran x A x B = x A x B
11 2 10 eqtr4i x A B = ran x A x B