Metamath Proof Explorer


Theorem dfima2

Description: Alternate definition of image. Compare definition (d) of Enderton p. 44. (Contributed by NM, 19-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfima2 A B = y | x B x A y

Proof

Step Hyp Ref Expression
1 df-ima A B = ran A B
2 dfrn2 ran A B = y | x x A B y
3 brres y V x A B y x B x A y
4 3 elv x A B y x B x A y
5 4 exbii x x A B y x x B x A y
6 df-rex x B x A y x x B x A y
7 5 6 bitr4i x x A B y x B x A y
8 7 abbii y | x x A B y = y | x B x A y
9 1 2 8 3eqtri A B = y | x B x A y