theorem elTail (S: set) (n: nat): $ n e. Tail S <-> suc n e. S $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | _1 = n -> _1 = n |
|
| 2 | 1 | suceqd | _1 = n -> suc _1 = suc n |
| 3 | 2 | eleq1d | _1 = n -> (suc _1 e. S <-> suc n e. S) |
| 4 | 3 | elabe | n e. {_1 | suc _1 e. S} <-> suc n e. S |
| 5 | 4 | conv Tail | n e. Tail S <-> suc n e. S |