Metamath Proof Explorer


Theorem rabimbieq

Description: Restricted equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 22-Jul-2021)

Ref Expression
Hypotheses rabimbieq.1 B = x A | φ
rabimbieq.2 x A φ ψ
Assertion rabimbieq B = x A | ψ

Proof

Step Hyp Ref Expression
1 rabimbieq.1 B = x A | φ
2 rabimbieq.2 x A φ ψ
3 2 rabbiia x A | φ = x A | ψ
4 1 3 eqtri B = x A | ψ