theorem elneq2d (G: wff) (a b c: nat): $ G -> b = c $ > $ G -> (a e. b <-> a e. c) $;
G -> a = a
G -> b = c
G -> (a e. b <-> a e. c)