Theorem abid2 2874

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  csbid  3864  csbconstg  3870  csbie  3886  abss  4016  ssab  4017  abssi  4022  notab  4268  dfrab3  4273  notrab  4276  eusn  4689  uniintsn  4942  axrep6g  5237  csbexg  5257  imai  6041  dffv4  6839  orduniss2  7785  dfixp  8849  euen1b  8977  modom2  9164  pwfir  9229  infmap2  10139  ustfn  24161  ustn0  24180  lrrecse  27953  lrrecpred  27955  fpwrelmap  32827  eulerpartlemgvv  34558  ballotlem2  34671  dffv5  36142  ptrest  37874  cnambfre  37923  cnvepresex  38591  pmapglb  40150  polval2N  40286  rngunsnply  43530  iocinico  43573