Description: Two ways to express membership equivalence relation on its domain quotient. (Contributed by Peter Mazsa, 26-Sep-2021) (Revised by Peter Mazsa, 17-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | eqvreldmqs |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-coeleqvrel | ||
2 | 1 | bicomi | |
3 | dmqs1cosscnvepreseq | ||
4 | 2 3 | anbi12i |