Theorem brressn

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

	Ref	Expression
Assertion	brressn	|- ( ( B e. V /\ C e. W ) -> ( B ( R |` { A } ) C <-> ( B = A /\ B R C ) ) )

Proof

Step	Hyp	Ref	Expression
1		brres	|- ( C e. W -> ( B ( R |` { A } ) C <-> ( B e. { A } /\ B R C ) ) )
2	1	adantl	|- ( ( B e. V /\ C e. W ) -> ( B ( R |` { A } ) C <-> ( B e. { A } /\ B R C ) ) )
3		elsng	|- ( B e. V -> ( B e. { A } <-> B = A ) )
4	3	adantr	|- ( ( B e. V /\ C e. W ) -> ( B e. { A } <-> B = A ) )
5	4	anbi1d	|- ( ( B e. V /\ C e. W ) -> ( ( B e. { A } /\ B R C ) <-> ( B = A /\ B R C ) ) )
6	2 5	bitrd	|- ( ( B e. V /\ C e. W ) -> ( B ( R |` { A } ) C <-> ( B = A /\ B R C ) ) )