Theorem opabresidOLD

Description: Obsolete version of opabresid as of 26-Dec-2023. (Contributed by FL, 25-Apr-2012) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	opabresidOLD	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) } = ( I ↾ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		resopab	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = 𝑥 } ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) }
2		equcom	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
3	2	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = 𝑥 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
4		df-id	⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
5	3 4	eqtr4i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = 𝑥 } = I
6	5	reseq1i	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = 𝑥 } ↾ 𝐴 ) = ( I ↾ 𝐴 )
7	1 6	eqtr3i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) } = ( I ↾ 𝐴 )