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 e. V -> ( [ A ] R e. ( dom R /. R ) <-> A e. dom R ) )

Proof

Step	Hyp	Ref	Expression
1		resexg	|- ( R e. V -> ( R |` dom R ) e. _V )
2		eqid	|- dom R = dom R
3		ecelqsdmb	|- ( ( ( R |` dom R ) e. _V /\ dom R = dom R ) -> ( [ A ] R e. ( dom R /. R ) <-> A e. dom R ) )
4	1 2 3	sylancl	|- ( R e. V -> ( [ A ] R e. ( dom R /. R ) <-> A e. dom R ) )