Theorem elrnressn

Description: Element of the range of a restriction to a singleton. (Contributed by Peter Mazsa, 12-Jun-2024)

	Ref	Expression
Assertion	elrnressn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ∈ ran ( 𝑅 ↾ { 𝐴 } ) ↔ 𝐴 𝑅 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elrnres	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∈ ran ( 𝑅 ↾ { 𝐴 } ) ↔ ∃ 𝑥 ∈ { 𝐴 } 𝑥 𝑅 𝐵 ) )
2		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝑅 𝐵 ↔ 𝐴 𝑅 𝐵 ) )
3	2	rexsng	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ { 𝐴 } 𝑥 𝑅 𝐵 ↔ 𝐴 𝑅 𝐵 ) )
4	1 3	sylan9bbr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ∈ ran ( 𝑅 ↾ { 𝐴 } ) ↔ 𝐴 𝑅 𝐵 ) )