Theorem abid2 1627

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 177	. . 3 |- (x e. A <-> x e. A)
2	1	abbi2i 1621	. 2 |- A = {x | x e. A}
3	2	eqcomi 1526	1 |- {x | x e. A} = A

Syntax hints:   = wceq 997   e. wcel 999  {cab 1509

This theorem is referenced by:  abidhb 1959  hbsbc1gd 2033  hbsbcgd 2034  csbid 2056  csbexg 2059  csbconstgf 2061  abss 2168  ssab 2169  abssi 2173  inrab2 2323  dfrab2 2325  opabss 2723  dfepfr 2989  epfrc 2990  orduniss2 3147  imai 3474  ecid 4361  qsid 4362  cardval 4889  cardval2 4920  sumex 7071  infmap2 7673  lpval 7828

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518

Copyright terms: Public domain