Theorem abid2 2745

Description: A simplification of class abstraction. Commuted form of abid1 2744. See comments there. (Contributed by NM, 26-Dec-1993.)

Assertion

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

Distinct variable group:   x, A

Proof of Theorem abid2

Step	Hyp	Ref	Expression
1		abid1 2744	. 2 |- A = { x | x e. A }
2	1	eqcomi 2631	1 |- { x | x e. A } = A

Syntax hints:   = wceq 1483   e. wcel 1990   {cab 2608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618

This theorem is referenced by:  csbid  3541  abss  3671  ssab  3672  abssi  3677  notab  3897  dfrab3  3902  notrab  3904  eusn  4265  uniintsn  4514  iunid  4575  csbexg  4792  imai  5478  dffv4  6188  orduniss2  7033  dfixp  7910  euen1b  8027  modom2  8162  infmap2  9040  cshwsexa  13570  ustfn  22005  ustn0  22024  fpwrelmap  29508  eulerpartlemgvv  30438  ballotlem2  30550  dffv5  32031  ptrest  33408  cnambfre  33458  cnvepresex  34104  pmapglb  35056  polval2N  35192  rngunsnply  37743  iocinico  37797