Description: The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999) (Revised by Mario Carneiro, 9-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | snec.1 | ⊢ 𝐴 ∈ V | |
Assertion | snec | ⊢ { [ 𝐴 ] 𝑅 } = ( { 𝐴 } / 𝑅 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snec.1 | ⊢ 𝐴 ∈ V | |
2 | eceq1 | ⊢ ( 𝑥 = 𝐴 → [ 𝑥 ] 𝑅 = [ 𝐴 ] 𝑅 ) | |
3 | 2 | eqeq2d | ⊢ ( 𝑥 = 𝐴 → ( 𝑦 = [ 𝑥 ] 𝑅 ↔ 𝑦 = [ 𝐴 ] 𝑅 ) ) |
4 | 1 3 | rexsn | ⊢ ( ∃ 𝑥 ∈ { 𝐴 } 𝑦 = [ 𝑥 ] 𝑅 ↔ 𝑦 = [ 𝐴 ] 𝑅 ) |
5 | 4 | abbii | ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝐴 } 𝑦 = [ 𝑥 ] 𝑅 } = { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } |
6 | df-qs | ⊢ ( { 𝐴 } / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ { 𝐴 } 𝑦 = [ 𝑥 ] 𝑅 } | |
7 | df-sn | ⊢ { [ 𝐴 ] 𝑅 } = { 𝑦 ∣ 𝑦 = [ 𝐴 ] 𝑅 } | |
8 | 5 6 7 | 3eqtr4ri | ⊢ { [ 𝐴 ] 𝑅 } = ( { 𝐴 } / 𝑅 ) |