Description: A set is equal to its quotient set modulo the converse membership relation. (Note: the converse membership relation is not an equivalence relation.) (Contributed by NM, 13-Aug-1995) (Revised by Mario Carneiro, 9-Jul-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | qsid | ⊢ ( 𝐴 / ◡ E ) = 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | ⊢ 𝑥 ∈ V | |
| 2 | 1 | ecid | ⊢ [ 𝑥 ] ◡ E = 𝑥 |
| 3 | 2 | eqeq2i | ⊢ ( 𝑦 = [ 𝑥 ] ◡ E ↔ 𝑦 = 𝑥 ) |
| 4 | equcom | ⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 ) | |
| 5 | 3 4 | bitri | ⊢ ( 𝑦 = [ 𝑥 ] ◡ E ↔ 𝑥 = 𝑦 ) |
| 6 | 5 | rexbii | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] ◡ E ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = 𝑦 ) |
| 7 | vex | ⊢ 𝑦 ∈ V | |
| 8 | 7 | elqs | ⊢ ( 𝑦 ∈ ( 𝐴 / ◡ E ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] ◡ E ) |
| 9 | risset | ⊢ ( 𝑦 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = 𝑦 ) | |
| 10 | 6 8 9 | 3bitr4i | ⊢ ( 𝑦 ∈ ( 𝐴 / ◡ E ) ↔ 𝑦 ∈ 𝐴 ) |
| 11 | 10 | eqriv | ⊢ ( 𝐴 / ◡ E ) = 𝐴 |