Description: Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | dfqs2 | ⊢ ( 𝐴 / 𝑅 ) = ran ( 𝑥 ∈ 𝐴 ↦ [ 𝑥 ] 𝑅 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-qs | ⊢ ( 𝐴 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } | |
2 | eqid | ⊢ ( 𝑥 ∈ 𝐴 ↦ [ 𝑥 ] 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ [ 𝑥 ] 𝑅 ) | |
3 | 2 | rnmpt | ⊢ ran ( 𝑥 ∈ 𝐴 ↦ [ 𝑥 ] 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } |
4 | 1 3 | eqtr4i | ⊢ ( 𝐴 / 𝑅 ) = ran ( 𝑥 ∈ 𝐴 ↦ [ 𝑥 ] 𝑅 ) |