theorem eleq1 (A: set) (a b: nat): $ a = b -> (a e. A <-> b e. A) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax_8 | a = b -> a e. A -> b e. A |
|
| 2 | ax_8 | b = a -> b e. A -> a e. A |
|
| 3 | eqcom | a = b -> b = a |
|
| 4 | 2, 3 | syl | a = b -> b e. A -> a e. A |
| 5 | 1, 4 | ibid | a = b -> (a e. A <-> b e. A) |