Theorem brres

Description: Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022)

	Ref	Expression
Assertion	brres	|- ( C e. V -> ( B ( R |` A ) C <-> ( B e. A /\ B R C ) ) )

Proof

Step	Hyp	Ref	Expression
1		opelres	|- ( C e. V -> ( <. B , C >. e. ( R |` A ) <-> ( B e. A /\ <. B , C >. e. R ) ) )
2		df-br	|- ( B ( R |` A ) C <-> <. B , C >. e. ( R |` A ) )
3		df-br	|- ( B R C <-> <. B , C >. e. R )
4	3	anbi2i	|- ( ( B e. A /\ B R C ) <-> ( B e. A /\ <. B , C >. e. R ) )
5	1 2 4	3bitr4g	|- ( C e. V -> ( B ( R |` A ) C <-> ( B e. A /\ B R C ) ) )