theorem eqab1d (A: set) (G: wff) {x: nat} (p: wff x): $ G -> (p <-> x e. A) $ > $ G -> {x | p} == A $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h | G -> (p <-> x e. A) |
|
2 | 1 | bicomd | G -> (x e. A <-> p) |
3 | 2 | eqab2d | G -> A == {x | p} |
4 | 3 | eqscomd | G -> {x | p} == A |