Metamath Proof Explorer


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 ( 𝑥𝐴 ↦ [ 𝑥 ] 𝑅 )