Metamath Proof Explorer


Theorem rabbieq

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 }

Proof

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 }