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\in \left\{x|\phi \right\}\leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		df-clab	$$⊢x\in \left\{x|\phi \right\}\leftrightarrow \left[x/x\right]\phi$$
2		sbid	$$⊢\left[x/x\right]\phi \leftrightarrow \phi$$
3	1 2	bitri	$$⊢x\in \left\{x|\phi \right\}\leftrightarrow \phi$$