Theorem abid2 2868

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  {cab 2709

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806

This theorem is referenced by:  csbid  3858  csbconstg  3864  csbie  3880  abss  4009  ssab  4010  abssi  4015  notab  4261  dfrab3  4266  notrab  4269  eusn  4680  uniintsn  4933  axrep6g  5226  csbexg  5246  imai  6022  dffv4  6819  orduniss2  7763  dfixp  8823  euen1b  8950  modom2  9136  pwfir  9201  infmap2  10108  ustfn  24117  ustn0  24136  lrrecse  27885  lrrecpred  27887  fpwrelmap  32716  eulerpartlemgvv  34389  ballotlem2  34502  dffv5  35966  ptrest  37669  cnambfre  37718  cnvepresex  38378  pmapglb  39879  polval2N  40015  rngunsnply  43272  iocinico  43315