Theorem abid 2226

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 2225	. 2 |- ( x e. { x | ph } <-> [ x / x ] ph )
2		sbid 1827	. 2 |- ( [ x / x ] ph <-> ph )
3	1, 2	bitri 184	1 |- ( x e. { x | ph } <-> ph )

Syntax hints:   <-> wb 105   [wsb 1815   e. wcel 2209   {cab 2224

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 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583

This theorem depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225

This theorem is referenced by:  abeq2  2347  abeq2i  2349  abeq1i  2350  abeq2d  2351  eqabrd  2378  abid2f  2418  elabgt  2967  elabgf  2968  ralab2  2990  rexab2  2992  sbccsbg  3176  sbccsb2g  3177  ss2ab  3316  abn0r  3546  abn0m  3547  tpid3g  3823  eluniab  3942  elintab  3976  iunab  4054  iinab  4069  intexabim  4283  iinexgm  4285  opm  4369  finds2  4743  dmmrnm  4996  iotaexab  5351  sniota  5363  eusvobj2  6061  eloprabga  6165  modom  7098  indpi  7699  4sqlem12  13159  elabgf0  16719