Theorem abid2 1577

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 1571	. 2 |- A = {x | x e. A}
3	2	eqcomi 1476	1 |- {x | x e. A} = A

Syntax hints:   = wceq 954   e. wcel 956  {cab 1461

This theorem is referenced by:  abidhb 1908  hbsbc1gd 1979  hbsbcgd 1980  csbid 2001  csbexg 2004  csbconstgf 2006  abss 2113  ssab 2114  abssi 2118  inrab2 2268  dfrab2 2270  opabss 2663  dfepfr 2927  epfrc 2928  orduniss2 3085  imai 3409  ecid 4290  qsid 4291  cardval 4806  cardval2 4835  sumex 6927  infmap2 7531  lpval 7693

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470

Copyright terms: Public domain