Metamath Proof Explorer


Theorem rabbiia

Description: Equivalent formulas yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999) (Proof shortened by Wolf Lammen, 12-Jan-2025)

Ref Expression
Hypothesis rabbiia.1 x A φ ψ
Assertion rabbiia x A | φ = x A | ψ

Proof

Step Hyp Ref Expression
1 rabbiia.1 x A φ ψ
2 1 pm5.32i x A φ x A ψ
3 2 rabbia2 x A | φ = x A | ψ