theorem eleq2d (A B: set) (G: wff) (a: nat): $ G -> A == B $ > $ G -> (a e. A <-> a e. B) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 |
A == B -> (a e. A <-> a e. B) |
||
2 |
hyp h |
G -> A == B |
|
3 |
G -> (a e. A <-> a e. B) |