Theorem abid 1873

Description: Simplification of class abstraction notation when the free and bound variables are identical.

Assertion

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

Proof of Theorem abid

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

Syntax hints:   <-> wb 163   e. wcel 1300  [wsbc 1534  {cab 1871

This theorem is referenced by:  abeq2 1999  abeq2i 2001  abeq1i 2002  abeq2d 2003  eq2ab 2004  abid2f 2012  elabgt 2400  elabgtOLD 2401  elabf 2402  elabgf 2404  sbccsbg 2565  sbccsb2g 2566  ss2ab 2675  abn0 2892  tpid3g 3115  eluniab 3189  reucl 3213  elintab 3227  ssintab 3233  ssintabOLD 3234  zfrep4 3436  euuni 3807  eufromeq4 3831  euobj2 3835  onminex 3888  finds2 3981  eloprabg 4936  iunon 5114  iinon 5115  iunfi 5659  en3lplem2 5757  scott0 5847  scottexs 5848  scott0s 5849  cp 5852  ac6lem 5916  bnj63 12432  bnj78 12439  bnj79OLD 12441  bnj100 12449  bnj99 12450  bnj1144 12941  bnj1343 13067  omslim2 14421  dominc 14622  rninc 14623  cntrsetlem 14999  firnfi3 15743  tpid3gVD 16666  en3lplem2VD 16668  strdif 16719

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-12 1310  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872

Copyright terms: Public domain