Theorem abid2 1583

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

Syntax hints:   = wceq 958   e. wcel 960  {cab 1466

This theorem is referenced by:  abidhb 1915  hbsbc1gd 1986  hbsbcgd 1987  csbid 2008  csbexg 2011  csbconstgf 2013  abss 2120  ssab 2121  abssi 2125  inrab2 2275  dfrab2 2277  opabss 2673  dfepfr 2938  epfrc 2939  orduniss2 3096  imai 3423  ecid 4306  qsid 4307  cardval 4836  cardval2 4866  sumex 6981  infmap2 7583  lpval 7740

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475

Copyright terms: Public domain