Metamath Proof Explorer


Theorem dfimafnf

Description: Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006) (Revised by Thierry Arnoux, 24-Apr-2017)

Ref Expression
Hypotheses dfimafnf.1 _ x A
dfimafnf.2 _ x F
Assertion dfimafnf Fun F A dom F F A = y | x A y = F x

Proof

Step Hyp Ref Expression
1 dfimafnf.1 _ x A
2 dfimafnf.2 _ x F
3 ssel A dom F z A z dom F
4 eqcom F z = y y = F z
5 funbrfvb Fun F z dom F F z = y z F y
6 4 5 syl5bbr Fun F z dom F y = F z z F y
7 6 ex Fun F z dom F y = F z z F y
8 3 7 syl9r Fun F A dom F z A y = F z z F y
9 8 imp31 Fun F A dom F z A y = F z z F y
10 9 rexbidva Fun F A dom F z A y = F z z A z F y
11 10 abbidv Fun F A dom F y | z A y = F z = y | z A z F y
12 dfima2 F A = y | z A z F y
13 11 12 syl6reqr Fun F A dom F F A = y | z A y = F z
14 nfcv _ z A
15 nfcv _ x z
16 2 15 nffv _ x F z
17 16 nfeq2 x y = F z
18 nfv z y = F x
19 fveq2 z = x F z = F x
20 19 eqeq2d z = x y = F z y = F x
21 14 1 17 18 20 cbvrexfw z A y = F z x A y = F x
22 21 abbii y | z A y = F z = y | x A y = F x
23 13 22 syl6eq Fun F A dom F F A = y | x A y = F x