Theorem abid2 1580

Description: A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35.

Assertion

Ref	Expression
abid2	|- {x | x e. A} = A

Distinct variable group:   x,A

Proof of Theorem abid2

Step	Hyp	Ref	Expression
1		pm4.2 170	. . 3 |- (x e. A <-> x e. A)
2	1	abbi2i 1574	. 2 |- A = {x | x e. A}
3	2	eqcomi 1479	1 |- {x | x e. A} = A

Syntax hints:   = wceq 956   e. wcel 958  {cab 1463

This theorem is referenced by:  abidhb 1912  hbsbc1gd 1983  hbsbcgd 1984  csbid 2005  csbexg 2008  csbconstgf 2010  abss 2117  ssab 2118  abssi 2122  inrab2 2272  dfrab2 2274  opabss 2668  dfepfr 2932  epfrc 2933  orduniss2 3090  imai 3417  ecid 4300  qsid 4301  cardval 4826  cardval2 4855  sumex 6981  infmap2 7581  lpval 7743

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472

Copyright terms: Public domain