Metamath Proof Explorer


Theorem eqvreldmqs

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 EqvRel E -1 A dom E -1 A / E -1 A = A CoElEqvRel A A / A = A

Proof

Step Hyp Ref Expression
1 df-coeleqvrel CoElEqvRel A EqvRel E -1 A
2 1 bicomi EqvRel E -1 A CoElEqvRel A
3 dmqs1cosscnvepreseq dom E -1 A / E -1 A = A A / A = A
4 2 3 anbi12i EqvRel E -1 A dom E -1 A / E -1 A = A CoElEqvRel A A / A = A