Theorem abid2 2876

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814

This theorem is referenced by:  csbid  3844  csbconstg  3850  csbie  3866  abss  3993  ssab  3994  abssi  3999  notab  4242  dfrab3  4247  notrab  4250  eusn  4662  uniintsn  4915  axrep6g  5212  csbexg  5232  imai  6026  dffv4  6824  orduniss2  7773  dfixp  8837  euen1b  8965  modom2  9152  pwfir  9217  infmap2  10130  ustfn  24185  ustn0  24204  lrrecse  27952  lrrecpred  27954  fpwrelmap  32825  eulerpartlemgvv  34560  ballotlem2  34673  dffv5  36150  ptrest  37986  cnambfre  38035  cnvepresex  38703  pmapglb  40262  polval2N  40398  rngunsnply  43614  iocinico  43657