Theorem dfqs3

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

	Ref	Expression
Assertion	dfqs3	$$⊢A/R=\bigcup _{x\in A}\left\{\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		iunsn	$$⊢\bigcup _{x\in A}\left\{\left[x\right]R\right\}=\left\{y|\exists x\in Ay=\left[x\right]R\right\}$$
3	1 2	eqtr4i	$$⊢A/R=\bigcup _{x\in A}\left\{\left[x\right]R\right\}$$