This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( 𝑅 ∈ 𝑉 → ( [ 𝐴 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ↔ 𝐴 ∈ dom 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		resexg	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↾ dom 𝑅 ) ∈ V )
2		eqid	⊢ dom 𝑅 = dom 𝑅
3		ecelqsdmb	⊢ ( ( ( 𝑅 ↾ dom 𝑅 ) ∈ V ∧ dom 𝑅 = dom 𝑅 ) → ( [ 𝐴 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ↔ 𝐴 ∈ dom 𝑅 ) )
4	1 2 3	sylancl	⊢ ( 𝑅 ∈ 𝑉 → ( [ 𝐴 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ↔ 𝐴 ∈ dom 𝑅 ) )