Metamath Proof Explorer

Theorem abidnf

Description: Identity used to create closed-form versions of bound-variable hypothesis builders for class expressions. (Contributed by NM, 10-Nov-2005) (Proof shortened by Mario Carneiro, 12-Oct-2016)

Ref Expression
Assertion abidnf _ x A z | x z A = A


Step Hyp Ref Expression
1 sp x z A z A
2 nfcr _ x A x z A
3 2 nf5rd _ x A z A x z A
4 1 3 impbid2 _ x A x z A z A
5 4 abbi1dv _ x A z | x z A = A