Metamath Proof Explorer

Theorem eceldmqs

Description: R -coset in its domain quotient. This is the bridge between A in the domain and its block [ A ] R in its domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019) (Revised by Peter Mazsa, 22-Nov-2025)

Ref Expression
Assertion eceldmqs ⊢ R ∈ V → A R ∈ dom ⁡ R / R ↔ A ∈ dom ⁡ R

Proof

Step Hyp Ref Expression
1 resexg ⊢ R ∈ V → R ↾ dom ⁡ R ∈ V
2 eqid ⊢ dom ⁡ R = dom ⁡ R
3 ecelqsdmb ⊢ R ↾ dom ⁡ R ∈ V ∧ dom ⁡ R = dom ⁡ R → A R ∈ dom ⁡ R / R ↔ A ∈ dom ⁡ R
4 1 2 3 sylancl ⊢ R ∈ V → A R ∈ dom ⁡ R / R ↔ A ∈ dom ⁡ R