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