theorem elrapp (F: set) (a b: nat): $ b e. F @' a <-> a, b e. F $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | _1 = b -> _1 = b |
|
| 2 | 1 | preq2d | _1 = b -> a, _1 = a, b |
| 3 | 2 | eleq1d | _1 = b -> (a, _1 e. F <-> a, b e. F) |
| 4 | 3 | elabe | b e. {_1 | a, _1 e. F} <-> a, b e. F |
| 5 | 4 | conv rapp | b e. F @' a <-> a, b e. F |