Theorem abid 2745

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 2742	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑)
2		sbid 2294	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
3	1, 2	bitri 278	1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 209  [wsb 2101   ∈ wcel 2147  {cab 2741

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742

This theorem is used by:  eqabrd  2905  eqabf  2955  abid2fOLD  2957  elabgf  3631  ralab2  3658  rexab2  3660  ss2ab  3989  ab0ALT  4333  sbccsb  4397  sbccsb2  4398  eluniab  4884  iunab  5013  iinab  5029  zfrep4  5250  rnep  5917  sniota  6552  opabiota  6993  eusvobj2  7438  eloprabga  7555  finds2  7937  ovmptss  8132  frrlem10  8344  en3lplem2  9644  scottabf  9969  scottexsOLD  9973  scott0bsOLD  9975  cp  9984  setrec2lem2  10006  cardprclem  10090  cfflb  10367  fin23lem29  10449  axdc3lem2  10559  4sqlem12  17166  xkococn  24012  ptcmplem4  24407  noinfbnd1lem1  28113  ofpreima  33334  algextdeglem6  34437  qqhval2  34697  esum2dlem  34807  sigaclcu2  34835  bnj1143  35503  bnj1366  35542  bnj906  35643  bnj1256  35728  bnj1259  35729  bnj1311  35737  mclsax  36514  ellines  37108  bj-csbsnlem  38006  bj-reabeq  38131  bj-velpwALT  38172  topdifinffinlem  38475  rdgssun  38506  finxpreclem6  38524  finxpnom  38529  ralssiun  38535  setindtrs  44236  rababg  44778  compab  45627  tpid3gVD  46026  en3lplem2VD  46028  permaxrep  46202  iunmapsn  46445  ssfiunibd  46540  absnsb  48312