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 )

This proof depends on syntax axioms:   <-> wb 105   [wsb 1815   e. wcel 2209   {cab 2224

This proof depends on 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 proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225

This theorem is used 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  3828  eluniab  3947  elintab  3981  iunab  4059  iinab  4074  intexabim  4288  iinexgm  4290  opm  4374  finds2  4748  dmmrnm  5001  iotaexab  5356  sniota  5368  eusvobj2  6071  eloprabga  6175  modom  7108  indpi  7709  4sqlem12  13181  elabgf0  16805