Description: Necessary and sufficient condition for a coset relation to be a converse reflexive relation. (Contributed by Peter Mazsa, 27-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | cnvrefrelcoss2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcoss | ||
2 | dfcnvrefrel2 | ||
3 | 1 2 | mpbiran2 | |
4 | cossssid | ||
5 | 3 4 | bitr4i |