Metamath Proof Explorer


Theorem opabresid

Description: The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012)

Ref Expression
Assertion opabresid ( I ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = 𝑥 ) }

Proof

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 ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = 𝑥 ) }