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