Theorem abid 2220

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

Assertion

Ref	Expression
abid	|- ( x e. { x | ph } <-> ph )

Proof of Theorem abid

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

Syntax hints:   <-> wb 105   [wsb 1811   e. wcel 2203   {cab 2218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219

This theorem is referenced by:  abeq2  2341  abeq2i  2343  abeq1i  2344  abeq2d  2345  eqabrd  2370  abid2f  2410  elabgt  2958  elabgf  2959  ralab2  2981  rexab2  2983  sbccsbg  3167  sbccsb2g  3168  ss2ab  3306  abn0r  3533  abn0m  3534  tpid3g  3807  eluniab  3926  elintab  3960  iunab  4038  iinab  4053  intexabim  4264  iinexgm  4266  opm  4350  finds2  4723  dmmrnm  4976  iotaexab  5331  sniota  5343  eusvobj2  6036  eloprabga  6140  modom  7061  indpi  7657  4sqlem12  13100  elabgf0  16549