Theorem abid2 2871

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {cab 2712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809

This theorem is referenced by:  csbid  3860  csbconstg  3866  csbie  3882  abss  4012  ssab  4013  abssi  4018  notab  4264  dfrab3  4269  notrab  4272  eusn  4685  uniintsn  4938  axrep6g  5233  csbexg  5253  imai  6031  dffv4  6829  orduniss2  7773  dfixp  8835  euen1b  8963  modom2  9150  pwfir  9215  infmap2  10125  ustfn  24144  ustn0  24163  lrrecse  27912  lrrecpred  27914  fpwrelmap  32761  eulerpartlemgvv  34482  ballotlem2  34595  dffv5  36065  ptrest  37759  cnambfre  37808  cnvepresex  38468  pmapglb  39969  polval2N  40105  rngunsnply  43353  iocinico  43396