Metamath Proof Explorer

Theorem abbid

Description: Equivalent wff's yield equal class abstractions (deduction form, with nonfreeness hypothesis). (Contributed by NM, 21-Jun-1993) (Revised by Mario Carneiro, 7-Oct-2016) Avoid ax-10 and ax-11 . (Revised by Wolf Lammen, 6-May-2023)

Ref Expression
Hypotheses abbid.1 x φ
abbid.2 φ ψ χ
Assertion abbid φ x | ψ = x | χ


Step Hyp Ref Expression
1 abbid.1 x φ
2 abbid.2 φ ψ χ
3 1 2 alrimi φ x ψ χ
4 abbi1 x ψ χ x | ψ = x | χ
5 3 4 syl φ x | ψ = x | χ