Theorem abid 2743

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

Assertion

Ref	Expression
abid	⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)

Proof of Theorem abid

Step	Hyp	Ref	Expression
1		df-clab 2740	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑)
2		sbid 2289	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
3	1, 2	bitri 277	1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 208  [wsb 2089   ∈ wcel 2141  {cab 2739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740

This theorem is referenced by:  eqabrd  2902  eqabf  2952  abid2fOLD  2954  elabgf  3633  ralab2  3659  rexab2  3661  ss2ab  4014  ab0ALT  4333  sbccsb  4389  sbccsb2  4390  eluniab  4878  iunab  5008  iinab  5024  zfrep4  5242  rnep  5901  sniota  6508  opabiota  6945  eusvobj2  7384  eloprabga  7501  finds2  7875  frrlem10  8271  en3lplem2  9565  scottexs  9842  scott0s  9843  cp  9846  cardprclem  9934  cfflb  10213  fin23lem29  10295  axdc3lem2  10405  4sqlem12  16975  xkococn  23700  ptcmplem4  24095  noinfbnd1lem1  27764  ofpreima  32817  algextdeglem6  33980  qqhval2  34240  esum2dlem  34350  sigaclcu2  34378  bnj1143  35049  bnj1366  35088  bnj906  35189  bnj1256  35274  bnj1259  35275  bnj1311  35283  mclsax  35883  ellines  36466  bj-csbsnlem  37352  bj-reabeq  37476  bj-velpwALT  37502  topdifinffinlem  37805  rdgssun  37836  finxpreclem6  37854  finxpnom  37859  ralssiun  37865  setindtrs  43566  rababg  44114  scottabf  44780  compab  44981  tpid3gVD  45381  en3lplem2VD  45383  permaxrep  45546  iunmapsn  45757  ssfiunibd  45852  absnsb  47585  setrec2lem2  50279