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 𝐵 = { 𝑥𝐴𝜑 }
rabbieq.2 ( 𝜑𝜓 )
Assertion rabbieq 𝐵 = { 𝑥𝐴𝜓 }

Proof

Step Hyp Ref Expression
1 rabbieq.1 𝐵 = { 𝑥𝐴𝜑 }
2 rabbieq.2 ( 𝜑𝜓 )
3 2 rabbii { 𝑥𝐴𝜑 } = { 𝑥𝐴𝜓 }
4 1 3 eqtri 𝐵 = { 𝑥𝐴𝜓 }