Metamath Proof Explorer

Theorem br1cossxrncnvepres

Description: <. B , C >. and <. D , E >. are cosets by a range Cartesian product with the restricted converse epsilon class: a binary relation. (Contributed by Peter Mazsa, 12-May-2021)

Ref Expression
Assertion br1cossxrncnvepres 
|- ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( `' _E |` A ) ) <. D , E >. <-> E. u e. A ( ( C e. u /\ u R B ) /\ ( E e. u /\ u R D ) ) ) )

Proof

Step Hyp Ref Expression
1 br1cossxrnres 
 |-  ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( `' _E |` A ) ) <. D , E >. <-> E. u e. A ( ( u `' _E C /\ u R B ) /\ ( u `' _E E /\ u R D ) ) ) )
2 brcnvep 
 |-  ( u e. _V -> ( u `' _E C <-> C e. u ) )
3 2 elv 
 |-  ( u `' _E C <-> C e. u )
4 3 anbi1i 
 |-  ( ( u `' _E C /\ u R B ) <-> ( C e. u /\ u R B ) )
5 brcnvep 
 |-  ( u e. _V -> ( u `' _E E <-> E e. u ) )
6 5 elv 
 |-  ( u `' _E E <-> E e. u )
7 6 anbi1i 
 |-  ( ( u `' _E E /\ u R D ) <-> ( E e. u /\ u R D ) )
8 4 7 anbi12i 
 |-  ( ( ( u `' _E C /\ u R B ) /\ ( u `' _E E /\ u R D ) ) <-> ( ( C e. u /\ u R B ) /\ ( E e. u /\ u R D ) ) )
9 8 rexbii 
 |-  ( E. u e. A ( ( u `' _E C /\ u R B ) /\ ( u `' _E E /\ u R D ) ) <-> E. u e. A ( ( C e. u /\ u R B ) /\ ( E e. u /\ u R D ) ) )
10 1 9 bitrdi 
 |-  ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( `' _E |` A ) ) <. D , E >. <-> E. u e. A ( ( C e. u /\ u R B ) /\ ( E e. u /\ u R D ) ) ) )