Description: Writing a set as a class abstraction. This theorem looks artificial but was added to characterize the class abstraction whose existence is proved in class2set . (Contributed by NM, 13-Dec-2005) (Proof shortened by Raph Levien, 30-Jun-2006)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | class2seteq | ⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V } = 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elex | ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V ) | |
| 2 | ax-1 | ⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ 𝐴 → 𝐴 ∈ V ) ) | |
| 3 | 2 | ralrimiv | ⊢ ( 𝐴 ∈ V → ∀ 𝑥 ∈ 𝐴 𝐴 ∈ V ) |
| 4 | rabid2im | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐴 ∈ V → 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V } ) | |
| 5 | 4 | eqcomd | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐴 ∈ V → { 𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V } = 𝐴 ) |
| 6 | 1 3 5 | 3syl | ⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V } = 𝐴 ) |