Metamath Proof Explorer

Theorem abid

Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 26-May-1993)

Ref Expression
Assertion abid x x | φ φ


Step Hyp Ref Expression
1 df-clab x x | φ x x φ
2 sbid x x φ φ
3 1 2 bitri x x | φ φ