Metamath Proof Explorer

Theorem br1cnvxrn2

Description: The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021)

Ref Expression
Assertion br1cnvxrn2 
|- ( B e. V -> ( A `' ( R |X. S ) B <-> E. y E. z ( A = <. y , z >. /\ B R y /\ B S z ) ) )

Proof

Step Hyp Ref Expression
1 xrnrel 
 |-  Rel ( R |X. S )
2 1 relbrcnv 
 |-  ( A `' ( R |X. S ) B <-> B ( R |X. S ) A )
3 brxrn2 
 |-  ( B e. V -> ( B ( R |X. S ) A <-> E. y E. z ( A = <. y , z >. /\ B R y /\ B S z ) ) )
4 2 3 bitrid 
 |-  ( B e. V -> ( A `' ( R |X. S ) B <-> E. y E. z ( A = <. y , z >. /\ B R y /\ B S z ) ) )