theorem exeqed (G: wff) {x: nat} (a: nat) (p: wff x) (q: wff): $ G /\ x = a -> (p <-> q) $ > $ G -> (E. x (x = a /\ p) <-> q) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsb3 | [a / x] p <-> E. x (x = a /\ p) |
|
2 | hyp e | G /\ x = a -> (p <-> q) |
|
3 | 2 | sbed | G -> ([a / x] p <-> q) |
4 | 1, 3 | syl5bbr | G -> (E. x (x = a /\ p) <-> q) |