Theorem dfqs2

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

	Ref	Expression
Assertion	dfqs2	⊢ ( 𝐴 / 𝑅 ) = ran ( 𝑥 ∈ 𝐴 ↦ [ 𝑥 ] 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		df-qs	⊢ ( 𝐴 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 }
2		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ [ 𝑥 ] 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ [ 𝑥 ] 𝑅 )
3	2	rnmpt	⊢ ran ( 𝑥 ∈ 𝐴 ↦ [ 𝑥 ] 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 }
4	1 3	eqtr4i	⊢ ( 𝐴 / 𝑅 ) = ran ( 𝑥 ∈ 𝐴 ↦ [ 𝑥 ] 𝑅 )