Description: The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | opabresid | ⊢ ( I ↾ 𝐴 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-id | ⊢ I = { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 = 𝑦 } | |
2 | equcom | ⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 ) | |
3 | 2 | opabbii | ⊢ { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 = 𝑦 } = { 〈 𝑥 , 𝑦 〉 ∣ 𝑦 = 𝑥 } |
4 | 1 3 | eqtri | ⊢ I = { 〈 𝑥 , 𝑦 〉 ∣ 𝑦 = 𝑥 } |
5 | 4 | reseq1i | ⊢ ( I ↾ 𝐴 ) = ( { 〈 𝑥 , 𝑦 〉 ∣ 𝑦 = 𝑥 } ↾ 𝐴 ) |
6 | resopab | ⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝑦 = 𝑥 } ↾ 𝐴 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) } | |
7 | 5 6 | eqtri | ⊢ ( I ↾ 𝐴 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) } |