Metamath Proof Explorer

Theorem rabbii

Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv . (Contributed by Peter Mazsa, 1-Nov-2019)

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


Step Hyp Ref Expression
1 rabbii.1 φ ψ
2 1 a1i x A φ ψ
3 2 rabbiia x A | φ = x A | ψ