Metamath Proof Explorer


Theorem rabbi

Description: Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbii . (Contributed by NM, 25-Nov-2013)

Ref Expression
Assertion rabbi x A ψ χ x A | ψ = x A | χ

Proof

Step Hyp Ref Expression
1 abbib x | x A ψ = x | x A χ x x A ψ x A χ
2 df-rab x A | ψ = x | x A ψ
3 df-rab x A | χ = x | x A χ
4 2 3 eqeq12i x A | ψ = x A | χ x | x A ψ = x | x A χ
5 df-ral x A ψ χ x x A ψ χ
6 pm5.32 x A ψ χ x A ψ x A χ
7 6 albii x x A ψ χ x x A ψ x A χ
8 5 7 bitri x A ψ χ x x A ψ x A χ
9 1 4 8 3bitr4ri x A ψ χ x A | ψ = x A | χ