Metamath Proof Explorer

Theorem br1cossincnvepres

Description: B and C are cosets by an intersection with the restricted converse epsilon class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion br1cossincnvepres 
|- ( ( B e. V /\ C e. W ) -> ( B ,~ ( R i^i ( `' _E |` A ) ) C <-> E. u e. A ( ( B e. u /\ u R B ) /\ ( C e. u /\ u R C ) ) ) )

Proof

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