Metamath Proof Explorer

Theorem brxrncnvep

Description: The range product with converse epsilon relation. (Contributed by Peter Mazsa, 22-Jun-2020) (Revised by Peter Mazsa, 22-Nov-2025)

Ref Expression
Assertion brxrncnvep 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( R |X. `' _E ) <. B , C >. <-> ( C e. A /\ A R B ) ) )

Proof

Step Hyp Ref Expression
1 brxrn 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( R |X. `' _E ) <. B , C >. <-> ( A R B /\ A `' _E C ) ) )
2 brcnvep 
 |-  ( A e. V -> ( A `' _E C <-> C e. A ) )
3 2 anbi1cd 
 |-  ( A e. V -> ( ( A R B /\ A `' _E C ) <-> ( C e. A /\ A R B ) ) )
4 3 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A R B /\ A `' _E C ) <-> ( C e. A /\ A R B ) ) )
5 1 4 bitrd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( R |X. `' _E ) <. B , C >. <-> ( C e. A /\ A R B ) ) )