theorem ellam (p: nat) {x: nat} (a: nat x): $ p e. \ x, a <-> E. x p = x, a $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeq1 | q = p -> (q = x, a <-> p = x, a) |
|
| 2 | 1 | exeqd | q = p -> (E. x q = x, a <-> E. x p = x, a) |
| 3 | 2 | elabe | p e. {q | E. x q = x, a} <-> E. x p = x, a |
| 4 | 3 | conv lam | p e. \ x, a <-> E. x p = x, a |