Theorem abid2 2873

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  csbid  3850  csbconstg  3856  csbie  3872  abss  4002  ssab  4003  abssi  4008  notab  4254  dfrab3  4259  notrab  4262  eusn  4674  uniintsn  4927  axrep6g  5225  csbexg  5245  imai  6039  dffv4  6837  orduniss2  7784  dfixp  8847  euen1b  8975  modom2  9162  pwfir  9227  infmap2  10139  ustfn  24167  ustn0  24186  lrrecse  27934  lrrecpred  27936  fpwrelmap  32806  eulerpartlemgvv  34520  ballotlem2  34633  dffv5  36104  ptrest  37940  cnambfre  37989  cnvepresex  38657  pmapglb  40216  polval2N  40352  rngunsnply  43597  iocinico  43640