Description: A class equals the union of its power class. Exercise 6(a) of Enderton p. 38. (Contributed by NM, 14-Oct-1996) (Proof shortened by Alan Sare, 28-Dec-2008)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | unipw | ⊢ ∪ 𝒫 𝐴 = 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eluni | ⊢ ( 𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 ) ) | |
| 2 | elelpwi | ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 ) → 𝑥 ∈ 𝐴 ) | |
| 3 | 2 | exlimiv | ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴 ) → 𝑥 ∈ 𝐴 ) |
| 4 | 1 3 | sylbi | ⊢ ( 𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴 ) |
| 5 | vsnid | ⊢ 𝑥 ∈ { 𝑥 } | |
| 6 | snelpwi | ⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ∈ 𝒫 𝐴 ) | |
| 7 | elunii | ⊢ ( ( 𝑥 ∈ { 𝑥 } ∧ { 𝑥 } ∈ 𝒫 𝐴 ) → 𝑥 ∈ ∪ 𝒫 𝐴 ) | |
| 8 | 5 6 7 | sylancr | ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴 ) |
| 9 | 4 8 | impbii | ⊢ ( 𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴 ) |
| 10 | 9 | eqriv | ⊢ ∪ 𝒫 𝐴 = 𝐴 |