Step |
Hyp |
Ref |
Expression |
1 |
|
df-ima |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } “ 𝐴 ) = ran ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↾ 𝐴 ) |
2 |
|
resopab |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↾ 𝐴 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } |
3 |
2
|
rneqi |
⊢ ran ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↾ 𝐴 ) = ran { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } |
4 |
|
rnopab |
⊢ ran { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } |
5 |
|
df-rex |
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) |
6 |
5
|
abbii |
⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } |
7 |
4 6
|
eqtr4i |
⊢ ran { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } |
8 |
1 3 7
|
3eqtri |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } |