Theorem br1cnvinxp

Description: Binary relation on the converse of an intersection with a Cartesian product. (Contributed by Peter Mazsa, 27-Jul-2019)

	Ref	Expression
Assertion	br1cnvinxp	|- ( C `' ( R i^i ( A X. B ) ) D <-> ( ( C e. B /\ D e. A ) /\ D R C ) )

Proof

Step	Hyp	Ref	Expression
1		relinxp	|- Rel ( R i^i ( A X. B ) )
2	1	relbrcnv	|- ( C `' ( R i^i ( A X. B ) ) D <-> D ( R i^i ( A X. B ) ) C )
3		brinxp2	|- ( D ( R i^i ( A X. B ) ) C <-> ( ( D e. A /\ C e. B ) /\ D R C ) )
4		ancom	|- ( ( D e. A /\ C e. B ) <-> ( C e. B /\ D e. A ) )
5	4	anbi1i	|- ( ( ( D e. A /\ C e. B ) /\ D R C ) <-> ( ( C e. B /\ D e. A ) /\ D R C ) )
6	2 3 5	3bitri	|- ( C `' ( R i^i ( A X. B ) ) D <-> ( ( C e. B /\ D e. A ) /\ D R C ) )