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 | eqsidd | _1 = n -> S == S |
|
| 4 | 2, 3 | eleqd | _1 = n -> (suc _1 e. S <-> suc n e. S) |
| 5 | 4 | elabe | n e. {_1 | suc _1 e. S} <-> suc n e. S |
| 6 | 5 | conv Tail | n e. Tail S <-> suc n e. S |