Description: Equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 8-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rabbieq.1 | |- B = { x e. A | ph } |
|
rabbieq.2 | |- ( ph <-> ps ) |
||
Assertion | rabbieq | |- B = { x e. A | ps } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabbieq.1 | |- B = { x e. A | ph } |
|
2 | rabbieq.2 | |- ( ph <-> ps ) |
|
3 | 2 | rabbii | |- { x e. A | ph } = { x e. A | ps } |
4 | 1 3 | eqtri | |- B = { x e. A | ps } |