Theorem ressn2

Description: A class ' R ' restricted to the singleton of the class ' A ' is the ordered pair class abstraction of the class ' A ' and the sets in relation ' R ' to ' A ' (and not in relation to the singleton ' { A } ' ). (Contributed by Peter Mazsa, 16-Jun-2024)

	Ref	Expression
Assertion	ressn2	⊢ ( 𝑅 ↾ { 𝐴 } ) = { ⟨ 𝑎 , 𝑢 ⟩ ∣ ( 𝑎 = 𝐴 ∧ 𝐴 𝑅 𝑢 ) }

Proof

Step	Hyp	Ref	Expression
1		dfres2	⊢ ( 𝑅 ↾ { 𝐴 } ) = { ⟨ 𝑎 , 𝑢 ⟩ ∣ ( 𝑎 ∈ { 𝐴 } ∧ 𝑎 𝑅 𝑢 ) }
2		velsn	⊢ ( 𝑎 ∈ { 𝐴 } ↔ 𝑎 = 𝐴 )
3	2	anbi1i	⊢ ( ( 𝑎 ∈ { 𝐴 } ∧ 𝑎 𝑅 𝑢 ) ↔ ( 𝑎 = 𝐴 ∧ 𝑎 𝑅 𝑢 ) )
4		eqbrb	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑎 𝑅 𝑢 ) ↔ ( 𝑎 = 𝐴 ∧ 𝐴 𝑅 𝑢 ) )
5	3 4	bitri	⊢ ( ( 𝑎 ∈ { 𝐴 } ∧ 𝑎 𝑅 𝑢 ) ↔ ( 𝑎 = 𝐴 ∧ 𝐴 𝑅 𝑢 ) )
6	5	opabbii	⊢ { ⟨ 𝑎 , 𝑢 ⟩ ∣ ( 𝑎 ∈ { 𝐴 } ∧ 𝑎 𝑅 𝑢 ) } = { ⟨ 𝑎 , 𝑢 ⟩ ∣ ( 𝑎 = 𝐴 ∧ 𝐴 𝑅 𝑢 ) }
7	1 6	eqtri	⊢ ( 𝑅 ↾ { 𝐴 } ) = { ⟨ 𝑎 , 𝑢 ⟩ ∣ ( 𝑎 = 𝐴 ∧ 𝐴 𝑅 𝑢 ) }