Description: Elementhood in a converse R -coset when R is a relation. (Contributed by Peter Mazsa, 9-Dec-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | releleccnv | |- ( Rel R -> ( A e. [ B ] `' R <-> A R B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv | |- Rel `' R |
|
2 | relelec | |- ( Rel `' R -> ( A e. [ B ] `' R <-> B `' R A ) ) |
|
3 | 1 2 | ax-mp | |- ( A e. [ B ] `' R <-> B `' R A ) |
4 | relbrcnvg | |- ( Rel R -> ( B `' R A <-> A R B ) ) |
|
5 | 3 4 | syl5bb | |- ( Rel R -> ( A e. [ B ] `' R <-> A R B ) ) |