Theorem dfqs2

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

	Ref	Expression
Assertion	dfqs2	$$⊢A/R=\mathrm{ran}\left(x\in A⟼\left[x\right]R\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-qs	$$⊢A/R=\left\{y|\exists x\in Ay=\left[x\right]R\right\}$$
2		eqid	$$⊢\left(x\in A⟼\left[x\right]R\right)=\left(x\in A⟼\left[x\right]R\right)$$
3	2	rnmpt	$$⊢\mathrm{ran}\left(x\in A⟼\left[x\right]R\right)=\left\{y|\exists x\in Ay=\left[x\right]R\right\}$$
4	1 3	eqtr4i	$$⊢A/R=\mathrm{ran}\left(x\in A⟼\left[x\right]R\right)$$