theorem elneq (a b c d: nat): $ a = b -> c = d -> (a e. c <-> b e. d) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anl | a = b /\ c = d -> a = b |
|
| 2 | anr | a = b /\ c = d -> c = d |
|
| 3 | 1, 2 | elneqd | a = b /\ c = d -> (a e. c <-> b e. d) |
| 4 | 3 | exp | a = b -> c = d -> (a e. c <-> b e. d) |