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 2747	1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Syntax hints:   = wceq 1539   ∈ wcel 2106  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816

This theorem is referenced by:  csbid  3845  csbconstg  3851  csbie  3868  abss  3994  ssab  3995  abssi  4003  notab  4238  dfrab3  4243  notrab  4245  eusn  4666  uniintsn  4918  iunid  4990  axrep6g  5217  csbexg  5234  imai  5982  dffv4  6771  orduniss2  7680  dfixp  8687  euen1b  8817  pwfir  8959  modom2  9024  infmap2  9974  cshwsexa  14537  ustfn  23353  ustn0  23372  fpwrelmap  31068  eulerpartlemgvv  32343  ballotlem2  32455  lrrecse  34099  lrrecpred  34101  dffv5  34226  ptrest  35776  cnambfre  35825  cnvepresex  36469  pmapglb  37784  polval2N  37920  rngunsnply  40998  iocinico  41043