Theorem dfqs2

Description: Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023)

	Ref	Expression
Assertion	dfqs2	|- ( A /. R ) = ran ( x e. A |-> [ x ] R )

Proof

Step	Hyp	Ref	Expression
1		df-qs	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
2		eqid	|- ( x e. A |-> [ x ] R ) = ( x e. A |-> [ x ] R )
3	2	rnmpt	|- ran ( x e. A |-> [ x ] R ) = { y | E. x e. A y = [ x ] R }
4	1 3	eqtr4i	|- ( A /. R ) = ran ( x e. A |-> [ x ] R )