theorem eueqd (_G: wff) {x: nat} (_p1 _p2: wff x):
$ _G -> (_p1 <-> _p2) $ >
$ _G -> (eu x _p1 <-> eu x _p2) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp _ph | _G -> (_p1 <-> _p2) |
|
| 2 | 1 | bieq1d | _G -> (_p1 <-> x = y <-> (_p2 <-> x = y)) |
| 3 | 2 | aleqd | _G -> (A. x (_p1 <-> x = y) <-> A. x (_p2 <-> x = y)) |
| 4 | 3 | exeqd | _G -> (E. y A. x (_p1 <-> x = y) <-> E. y A. x (_p2 <-> x = y)) |
| 5 | 4 | conv eu | _G -> (eu x _p1 <-> eu x _p2) |