Theorem abid2 2874

Description: A simplification of class abstraction. Commuted form of abid1 2873. 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 2873	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
2	1	eqcomi 2746	1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Syntax hints:   = wceq 1542   ∈ wcel 2114  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  csbid  3851  csbconstg  3857  csbie  3873  abss  4003  ssab  4004  abssi  4009  notab  4255  dfrab3  4260  notrab  4263  eusn  4675  uniintsn  4928  axrep6g  5226  csbexg  5246  imai  6034  dffv4  6832  orduniss2  7778  dfixp  8841  euen1b  8969  modom2  9156  pwfir  9221  infmap2  10133  ustfn  24180  ustn0  24199  lrrecse  27951  lrrecpred  27953  fpwrelmap  32824  eulerpartlemgvv  34539  ballotlem2  34652  dffv5  36123  ptrest  37957  cnambfre  38006  cnvepresex  38674  pmapglb  40233  polval2N  40369  rngunsnply  43618  iocinico  43661