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