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 ( 𝐴𝐵 ) = { 𝑦 ∣ ∃ 𝑥𝐵 𝑥 𝐴 𝑦 }

Proof

Step Hyp Ref Expression
1 df-ima ( 𝐴𝐵 ) = ran ( 𝐴𝐵 )
2 dfrn2 ran ( 𝐴𝐵 ) = { 𝑦 ∣ ∃ 𝑥 𝑥 ( 𝐴𝐵 ) 𝑦 }
3 brres ( 𝑦 ∈ V → ( 𝑥 ( 𝐴𝐵 ) 𝑦 ↔ ( 𝑥𝐵𝑥 𝐴 𝑦 ) ) )
4 3 elv ( 𝑥 ( 𝐴𝐵 ) 𝑦 ↔ ( 𝑥𝐵𝑥 𝐴 𝑦 ) )
5 4 exbii ( ∃ 𝑥 𝑥 ( 𝐴𝐵 ) 𝑦 ↔ ∃ 𝑥 ( 𝑥𝐵𝑥 𝐴 𝑦 ) )
6 df-rex ( ∃ 𝑥𝐵 𝑥 𝐴 𝑦 ↔ ∃ 𝑥 ( 𝑥𝐵𝑥 𝐴 𝑦 ) )
7 5 6 bitr4i ( ∃ 𝑥 𝑥 ( 𝐴𝐵 ) 𝑦 ↔ ∃ 𝑥𝐵 𝑥 𝐴 𝑦 )
8 7 abbii { 𝑦 ∣ ∃ 𝑥 𝑥 ( 𝐴𝐵 ) 𝑦 } = { 𝑦 ∣ ∃ 𝑥𝐵 𝑥 𝐴 𝑦 }
9 1 2 8 3eqtri ( 𝐴𝐵 ) = { 𝑦 ∣ ∃ 𝑥𝐵 𝑥 𝐴 𝑦 }