theorem elPower (A: set) (a: nat): $ a e. Power A <-> a C_ A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nseq | x = a -> x == a |
|
| 2 | 1 | sseq1d | x = a -> (x C_ A <-> a C_ A) |
| 3 | 2 | elabe | a e. {x | x C_ A} <-> a C_ A |
| 4 | 3 | conv Power | a e. Power A <-> a C_ A |