Theorem brressn

Description: Binary relation on a restriction to a singleton. (Contributed by Peter Mazsa, 11-Jun-2024)

	Ref	Expression
Assertion	brressn	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ( 𝑅 ↾ { 𝐴 } ) 𝐶 ↔ ( 𝐵 = 𝐴 ∧ 𝐵 𝑅 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		brres	⊢ ( 𝐶 ∈ 𝑊 → ( 𝐵 ( 𝑅 ↾ { 𝐴 } ) 𝐶 ↔ ( 𝐵 ∈ { 𝐴 } ∧ 𝐵 𝑅 𝐶 ) ) )
2	1	adantl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ( 𝑅 ↾ { 𝐴 } ) 𝐶 ↔ ( 𝐵 ∈ { 𝐴 } ∧ 𝐵 𝑅 𝐶 ) ) )
3		elsng	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ { 𝐴 } ↔ 𝐵 = 𝐴 ) )
4	3	adantr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ∈ { 𝐴 } ↔ 𝐵 = 𝐴 ) )
5	4	anbi1d	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝐵 ∈ { 𝐴 } ∧ 𝐵 𝑅 𝐶 ) ↔ ( 𝐵 = 𝐴 ∧ 𝐵 𝑅 𝐶 ) ) )
6	2 5	bitrd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ( 𝑅 ↾ { 𝐴 } ) 𝐶 ↔ ( 𝐵 = 𝐴 ∧ 𝐵 𝑅 𝐶 ) ) )