Theorem abid2 2882

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819

This theorem is referenced by:  csbid  3934  csbconstg  3940  csbie  3957  abss  4086  ssab  4087  abssi  4093  notab  4333  dfrab3  4338  notrab  4341  eusn  4755  uniintsn  5009  iunidOLD  5084  axrep6g  5311  csbexg  5328  imai  6105  dffv4  6919  orduniss2  7871  dfixp  8959  euen1b  9094  modom2  9310  pwfir  9385  infmap2  10288  cshwsexaOLD  14875  ustfn  24233  ustn0  24252  lrrecse  27995  lrrecpred  27997  fpwrelmap  32749  eulerpartlemgvv  34343  ballotlem2  34455  dffv5  35890  ptrest  37581  cnambfre  37630  cnvepresex  38292  pmapglb  39729  polval2N  39865  rngunsnply  43132  iocinico  43175