Description: Alternate definition of image. Compare definition (d) of Enderton p. 44. (Contributed by NM, 14-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfima3 | ⊢ ( 𝐴 “ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfima2 | ⊢ ( 𝐴 “ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑥 𝐴 𝑦 } | |
| 2 | df-br | ⊢ ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) | |
| 3 | 2 | rexbii | ⊢ ( ∃ 𝑥 ∈ 𝐵 𝑥 𝐴 𝑦 ↔ ∃ 𝑥 ∈ 𝐵 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) |
| 4 | df-rex | ⊢ ( ∃ 𝑥 ∈ 𝐵 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) | |
| 5 | 3 4 | bitri | ⊢ ( ∃ 𝑥 ∈ 𝐵 𝑥 𝐴 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) |
| 6 | 5 | abbii | ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑥 𝐴 𝑦 } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) } |
| 7 | 1 6 | eqtri | ⊢ ( 𝐴 “ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) } |