Description: Restricted converse subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | br1cnvssrres | |- ( B e. V -> ( B `' ( _S |` A ) C <-> ( C e. A /\ C C_ B ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relres | |- Rel ( _S |` A ) |
|
2 | 1 | relbrcnv | |- ( B `' ( _S |` A ) C <-> C ( _S |` A ) B ) |
3 | brssrres | |- ( B e. V -> ( C ( _S |` A ) B <-> ( C e. A /\ C C_ B ) ) ) |
|
4 | 2 3 | syl5bb | |- ( B e. V -> ( B `' ( _S |` A ) C <-> ( C e. A /\ C C_ B ) ) ) |