theorem eleq2 (A B: set) (a: nat): $ A == B -> (a e. A <-> a e. B) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1 | x = a -> (x e. A <-> a e. A) |
|
| 2 | eleq1 | x = a -> (x e. B <-> a e. B) |
|
| 3 | 1, 2 | bieqd | x = a -> (x e. A <-> x e. B <-> (a e. A <-> a e. B)) |
| 4 | 3 | eale | A. x (x e. A <-> x e. B) -> (a e. A <-> a e. B) |
| 5 | 4 | conv eqs | A == B -> (a e. A <-> a e. B) |