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 e. { x | ph } <-> ph )

Proof

Step Hyp Ref Expression
1 df-clab 
 |-  ( x e. { x | ph } <-> [ x / x ] ph )
2 sbid 
 |-  ( [ x / x ] ph <-> ph )
3 1 2 bitri 
 |-  ( x e. { x | ph } <-> ph )