Theorem abid2 2900

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

Assertion

Ref	Expression
abid2	⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem abid2

Step	Hyp	Ref	Expression
1		abid1 2899	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
2	1	eqcomi 2772	1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Syntax hints:   = wceq 1570   ∈ wcel 2143  {cab 2741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838

This theorem is referenced by:  csbid  3866  csbconstg  3872  csbie  3888  abss  4016  ssab  4017  abssi  4022  notab  4267  dfrab3  4272  notrab  4275  eusn  4696  uniintsn  4950  axrep6g  5251  csbexg  5273  imai  6076  dffv4  6878  orduniss2  7825  dfixp  8893  euen1b  9021  modom2  9208  pwfir  9272  infmap2  10196  ustfn  24359  ustn0  24378  lrrecse  28135  lrrecpred  28137  fpwrelmap  33078  eulerpartlemgvv  34766  ballotlem2  34879  dffv5  36414  ptrest  38290  cnambfre  38339  cnvepresex  39005  pmapglb  40564  polval2N  40700  rngunsnply  43916  iocinico  43959